snd_isOpenEmbedding_of_left — Mathlib

English

If f is an open embedding and g arbitrary, then pullback.snd f g is an open embedding.

Русский

Если f является открытым вложением, то pullback.snd f g — открытое вложение.

LaTeX

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

Lean4

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

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