map_subtype_embedding_Ici — Mathlib

English

For a predicate p on α and a family 𝒟, the map from the interval (Ici a) to the subtype Ici p is compatible; under a hp assumption, the map equals the interval (Ici a) mapped by the subtype embedding.

Русский

Для предиката p на α и семейства 𝒟 отображение из интервала (Ici a) в подтип Ici p совместимо; при условии hp отображение эквивалентно отображению через вложение подтипа.

LaTeX

$$$(Ici\\ a).map(Embedding.subtype\\, p)= (Ici\\ a)\\!:\\ Finset\\ α$$$

Lean4

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

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