property_of_mem_map_subtype — Mathlib

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

Похожие утверждения