pullback_fst_of_right — Mathlib

English

The first projection of the right pullback is an open immersion.

Русский

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

LaTeX

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

Lean4

/-- Open immersions are stable under base-change. -/
instance pullback_fst_of_right : LocallyRingedSpace.IsOpenImmersion (pullback.fst g f) :=
  by
  rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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