hasLimit_cospan_forget_of_right — Mathlib

English

If f is open immersion, the cospan g f has a limit after forgetting to LocallyRingedSpaces.

Русский

Если f открытое вложение, коспана g f имеет предел после забывания до локально кольцевых пространств.

LaTeX

$$HasLimit (cospan g f) forgetToLocallyRingedSpace$$

Lean4

instance hasLimit_cospan_forget_of_right : HasLimit (cospan g f ⋙ forget) :=
  by
  rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
  exact inferInstanceAs (HasLimit (cospan ((forget).map g) ((forget).map f)))

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