colimit_eq_iSup — Mathlib

English

For any diagram F: J ⥤ α into a complete lattice α, the colimit equals the supremum of the image, i.e., colim F = ∨_{j ∈ J} F(j).

Русский

Для диаграммы F: J ⥤ α в полной решётке α колимит равен верхней огибающей образов: colim F = ∨_{j ∈ J} F(j).

LaTeX

$$$\\forall (F: J ⥤ α), \\ \\operatorname{colimit} F = \\bigvee_{j \\in J} F(j).$$$

Lean4

/-- The colimit of a functor into a complete lattice is the supremum of the objects in the image.
-/
theorem colimit_eq_iSup (F : J ⥤ α) : colimit F = iSup F.obj :=
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) (colimitCocone F).isColimit).to_eq

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