English
If a is in the image of s.subtype p under Embedding.subtype, then p a holds.
Русский
Если элемент a принадлежит образу s.subtype p под Embedding.subtype, тогда выполняется p a.
LaTeX
$$$ a ∈ s.map (Embedding.subtype p) \\Rightarrow p a $$$
Lean4
/-- 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. -/
theorem property_of_mem_map_subtype {p : α → Prop} (s : Finset { x // p x }) {a : α}
(h : a ∈ s.map (Embedding.subtype _)) : p a :=
by
rcases mem_map.1 h with ⟨x, _, rfl⟩
exact x.2