isIso_π_of_isLimit — Mathlib

English

If c is a limit cone for F, then the component c.π.app i0 is an isomorphism.

Русский

Если c — пределной конус для F, то компонент c.π.app i0 является изоморфизмом.

LaTeX

$$$IsIso\bigl(c.\pi.\mathrm{app}\, i_0\bigr)$$$

Lean4

theorem isIso_π_of_isLimit {c : Cone F} (hc : IsLimit c) : IsIso (c.π.app i₀) :=
  by
  simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀, cone_π_app, coneπApp_eq_id, cone_pt,
    comp_id]
  infer_instance

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