asLimitConeIso — Mathlib

English

There is an isomorphism of cones X.asLimitCone ≅ limitCone X.diagram, whose underlying isomorphism is isoAsLimitConeLift.

Русский

Существуют изоморфизмы конусов X.asLimitCone ≅ limitCone X.diagram, базовый изоморфизм равен isoAsLimitConeLift.

LaTeX

$$$X.asLimitCone \cong \text{limitCone}(X.diagram)$$$

Lean4

/-- The isomorphism of cones `X.asLimitCone` and `Profinite.limitCone X.diagram`.
The underlying isomorphism is defeq to `X.isoAsLimitConeLift`.
-/
def asLimitConeIso : X.asLimitCone ≅ limitCone.{u, u} _ :=
  Limits.Cones.ext (isoAsLimitConeLift _) fun _ => rfl

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