notMem_map_subtype_of_not_property

English

If not p a, then a is not in the image of s.map Embedding.subtype p.

Русский

Если не выполняется p a, тогда a не принадлежит образу s.map Embedding.subtype p.

LaTeX

$$$ \\neg p a \\Rightarrow a ∉ s.map (Embedding.subtype p) $$$

Lean4

/-- If a `Finset` of a subtype is converted to the main type with
`Embedding.subtype`, the result does not contain any value that does
not satisfy the property of the subtype. -/
theorem notMem_map_subtype_of_not_property {p : α → Prop} (s : Finset { x // p x }) {a : α} (h : ¬p a) :
    a ∉ s.map (Embedding.subtype _) :=
  mt s.property_of_mem_map_subtype h

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