pullback_snd_of_left — Mathlib

English

The second projection of the left pullback is an open immersion.

Русский

Вторая проекция левой обратной диаграммы является открытым погружением.

LaTeX

$$$ IsOpenImmersion\; (pullback.snd\; f\; g) $$$

Lean4

/-- Open immersions are stable under base-change. -/
instance pullback_snd_of_left : LocallyRingedSpace.IsOpenImmersion (pullback.snd f g) :=
  by
  delta pullback.snd
  rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
  infer_instance

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