asLimit — Mathlib

English

`S.asLimitCone` is indeed a limit cone for the diagram of S.

Русский

S.asLimitCone действительно является пределом конуса диаграммы S.

LaTeX

$$$\\mathrm{IsLimit}(S.asLimitCone)$$$

Lean4

/-- `S.asLimitCone` is indeed a limit cone. -/
def asLimit : IsLimit S.asLimitCone :=
  S.asLimitAux.ofIsoLimit <|
    Cones.ext (lightToProfiniteFullyFaithful.preimageIso <| (Cones.forget _).mapIso S.isoMapCone)
      (fun _ ↦ by rw [← @Iso.inv_comp_eq]; rfl)

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