Theorems · Theorem · combinatorics

Finset.property_of_mem_map_subtype

∀ {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α},
  a ∈ Finset.map (Function.Embedding.subtype fun x => p x) s → p a

If a Finset of a subtype is converted to the main type with Embedding.subtype, all elements of the result have the property of the subtype.

Defined in

Mathlib.Data.Finset.Image

Cited by

2 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound