asLimitCone — Mathlib

English

A cone over X.diagram whose apex is X is constructed.

Русский

Составлен конус над X.diagram с вершиной X.

LaTeX

$$$\text{asLimitCone}(X) : \text{CategoryTheory.Limits.Cone}(X.diagnram)$$$

Lean4

/-- A cone over `X.diagram` whose cone point is `X`. -/
def asLimitCone : CategoryTheory.Limits.Cone X.diagram :=
  { pt := X
    π :=
      {
        app := fun S =>
          CompHausLike.ofHom (Y := X.diagram.obj S) _
            ⟨S.proj, IsLocallyConstant.continuous (S.proj_isLocallyConstant)⟩ } }

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