hasLimit_cospan_forget_of_left' — Mathlib

English

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

Русский

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

LaTeX

$$HasLimit (cospan g f) forgetToLocallyRingedSpace$$

Lean4

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

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