map_subtype_embedding_Iic — Mathlib

English

Let hp ensure upward-closure, then the image of the closed lower interval Iic(a) under the subtype embedding equals the closed lower interval Iic(a) in α.

Русский

Пусть hp обеспечивает восходящую замкнутость; тогда образ замкнутого нижнего интервала Iic(a) через вложение подтипа в α равен Iic(a) в α.

LaTeX

$$$(\\mathrm{Iic}(a)).\\mathrm{map}(\\mathrm{Embedding}.subtype(p)) = (\\mathrm{Iic}(a) : \\mathrm{Finset}\\, \\alpha)$$$

Lean4

theorem map_subtype_embedding_Iic (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iic a).map (Embedding.subtype p) = (Iic a : Finset α) :=
  by
  rw [subtype_Iic_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iic.1 hx) a.prop

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