hasLimit_cospan_forget_of_right' — Mathlib

English

If f is open immersion, the cospan g f has a limit in the forgetful setting via forgetToLocallyRingedSpace.

Русский

Если f открытое вложение, у коспана g f существует предел в забывающей постановке через forgetToLocallyRingedSpace.

LaTeX

$$HasLimit (cospan g f) forgetToLocallyRingedSpace$$

Lean4

instance hasLimit_cospan_forget_of_right' :
    HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) :=
  show HasLimit (cospan ((forget).map g) ((forget).map f)) from inferInstance

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