pullbackSndOfLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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