pullbackFstOfRight — Mathlib

English

Open immersions are stable under base change: the pullback projection to the right component is an open immersion.

Русский

Открытые вложения сохраняются при базовом изменении: проекция на правый компонент произведения является открытым вложением.

LaTeX

$$$\text{IsOpenImmersion}(\text{pullback.fst } g\ f)$$$

Lean4

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

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