hasLimit_cospan_forget_of_right — Mathlib

English

There is a limit for the cospan with the legs g and f after forgetting, i.e., HasLimit (cospan g f ⋙ forget).

Русский

Существует предел для касательной с ножками g и f после забывания, то есть HasLimit (cospan g f ⋙ forget).

LaTeX

$$$\\operatorname{HasLimit}(\\mathrm{cospan}\\ g\\ f\\;\\;\\mathrm{forget})$$$

Lean4

instance hasLimit_cospan_forget_of_right : HasLimit (cospan g f ⋙ forget) :=
  by
  have : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) :=
    by
    change HasLimit (cospan ((forget).map g) ((forget).map f))
    infer_instance
  apply hasLimit_of_iso (diagramIsoCospan _).symm

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