map_subtype_embedding_Iio — Mathlib

English

Similarly to Iic, for hp with x ≤ a, the image of Iio(a) under the subtype embedding equals the Iio(a) in α.

Русский

Аналогично Iic: образ Iio(a) через вложение подтипа равен Iio(a) в α при соответствующем hp.

LaTeX

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

Lean4

theorem map_subtype_embedding_Iio (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iio a).map (Embedding.subtype p) = (Iio a : Finset α) :=
  by
  rw [subtype_Iio_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iio.1 hx).le a.prop

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