asLimitAux — Mathlib

English

An auxiliary IsLimit for S.asLimitConeAux, constructed via reflected limits.

Русский

Вспомогательный предел для S.asLimitConeAux, полученный посредством отражённых пределов.

LaTeX

$$$\\mathrm{asLimitAux} : \\mathrm{IsLimit}(S.asLimitConeAux)$$$

Lean4

/-- `S.asLimitConeAux` is indeed a limit cone.
(Auxiliary definition, use `S.asLimit` instead.)
-/
def asLimitAux : IsLimit S.asLimitConeAux :=
  let hc : IsLimit (lightToProfinite.mapCone S.asLimitConeAux) := S.toLightDiagram.isLimit.ofIsoLimit S.isoMapCone.symm
  isLimitOfReflects lightToProfinite hc

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