cocone — Mathlib

English

The cocone constructed from U is in fact a colimit of the diagram diagram(U).

Русский

Кокон, построенный от U, на самом деле является колимитом диаграммы diagram(U).

LaTeX

$$$\mathrm{coconeIsColimit}(U) : \mathrm{IsColimit}(\mathrm{cocone}(U)).$$$

Lean4

/-- Given a function `U : ι → α` for `[CompleteLattice α]`,
`iSup U` provides a cocone over `diagram U`.
-/
@[simps]
def cocone : Cocone (diagram U) where
  pt := iSup U
  ι := { app := coconeιApp U }

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