hasColimits_of_completeLattice — Mathlib

English

Let α be a complete lattice. Then every small diagram F: J ⥤ α has a colimit; i.e., α has all small colimits.

Русский

Пусть α — полная решётка. Тогда для каждой малой категории J и любой F: J ⥤ α существует колимит; т.е. α имеет все малые колимиты.

LaTeX

$$$\\forall J [\\mathsf{Category}\,J],\\; \\forall F: J \\to α,\\ IsColimit(\\text{colimitCocone }F).$$$

Lean4

instance (priority := 100) hasColimits_of_completeLattice : HasColimitsOfSize.{w, w'} α where
  has_colimits_of_shape _ := { has_colimit := fun F => HasColimit.mk (colimitCocone F) }

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