isIso_π_app_of_isInitial — Mathlib

English

If F is a diagram and hc is a limit, then for an initial X, the component π.app X is an isomorphism.

Русский

Если F — диаграмма, а hc — предел, то компонент π.app X является изоморфизмом для начального X.

LaTeX

$$$\\text{hc : IsLimit } c \\land \\text{IsInitial } X \\Rightarrow \\IsIso (c.π.app X)$$$

Lean4

theorem isIso_π_app_of_isInitial {F : J ⥤ C} {c : Cone F} (hc : IsLimit c) (X : J) (hX : IsInitial X) :
    IsIso (c.π.app X) :=
  by
  change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom
  infer_instance

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