cone_fac — Mathlib

English

If F.cones is represented by X, every cone is the extension of the limit cone by the corresponding morphism: (limitCone h).extend (homOfCone h s) = s.

Русский

Если F.cones представлено X, то любой конус является продолжением лимит-конуса по соответствующему морфизму: (limitCone h).extend (homOfCone h s) = s.

LaTeX

$$$ (limitCone h).extend (homOfCone h s) = s $$$

Lean4

/-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
corresponding morphism. -/
theorem cone_fac (s : Cone F) : (limitCone h).extend (homOfCone h s) = s :=
  by
  rw [← coneOfHom_homOfCone h s]
  conv_lhs => simp only [homOfCone_coneOfHom]
  apply (coneOfHom_fac _ _).symm

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