pullback_to_base_isOpenImmersion — Mathlib

English

The projection from the pullback to the base along the left (or right) leg is an open immersion, under the corresponding hypothesis.

Русский

Проекция из обратной диаграммы в основание вдоль левой (или правой) ножки является открытым погружением при соответствующих предпосылках.

LaTeX

$$$ IsOpenImmersion( limit.\n \t.π( cospan(f,g) , WalkingCospan.one)) $$$

Lean4

instance pullback_to_base_isOpenImmersion [LocallyRingedSpace.IsOpenImmersion g] :
    LocallyRingedSpace.IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one) :=
  by
  rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
  infer_instance

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