fst_isOpenEmbedding_of_right — Mathlib

English

If g is an open embedding, then the fst projection from the pullback is an open embedding.

Русский

Если g является открытым вложением, то fst-проекция из предела является открытым вложением.

LaTeX

$$$ \text{IsOpenEmbedding}\big( \mathrm{pullback.fst} f g \big) $$$

Lean4

theorem fst_isOpenEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsOpenEmbedding g) :
    IsOpenEmbedding <| ⇑(pullback.fst f g) :=
  by
  convert
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl
        (by simp))
  simp [homeoOfIso, ← coe_comp]

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