asLimitindexConeIso — Mathlib

English

The lifted index cone is an isomorphism of cones.

Русский

Пусть поднятая индексная конуса является изоморфизмом конусов.

LaTeX

$$$\\text{IsIso}((\\text{Profinite.limitCone}(\\text{indexFunctor}(hC))).lift(\\text{indexCone}(hC)))$$$

Lean4

/-- The isomorphism of cones induced by `isoindexConeLift`. -/
noncomputable def asLimitindexConeIso : indexCone hC ≅ Profinite.limitCone.{u, u} _ :=
  Limits.Cones.ext (isoindexConeLift hC) fun _ => rfl

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