isoAsLimitConeLift — Mathlib

English

There is an isomorphism X ≅ (limitCone X.diagram).pt induced by lifting X.asLimitCone.

Русский

Существует изоморфизм X ≅ (limitCone X.diagram).pt, индуцируемый подъемом X.asLimitCone.

LaTeX

$$$X \cong (\limCone^{u,u} X.diagram).pt$$$

Lean4

/-- The isomorphism between `X` and the explicit limit of `X.diagram`,
induced by lifting `X.asLimitCone`.
-/
def isoAsLimitConeLift : X ≅ (limitCone.{u, u} X.diagram).pt :=
  asIso <| (limitConeIsLimit.{u, u} _).lift X.asLimitCone

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