pullbackToBaseIsOpenImmersion — Mathlib

English

If g is an open immersion, then the projection from the base change to the base is an open immersion.

Русский

Если g является открытым вложением, то проекция базового изменения к основанию является открытым вложением.

LaTeX

$$$\text{IsOpenImmersion}(\lim\.\pi (cospan\ f\ g)\ WalkingCospan.one)$$$

Lean4

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

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