hasLimits_of_completeLattice — Mathlib

English

Let α be a complete lattice. Then every small diagram F: J ⥤ α has a limit; equivalently, α has all small limits.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) hasLimits_of_completeLattice : HasLimitsOfSize.{w, w'} α where
  has_limits_of_shape
    _ :=
    { has_limit := fun F => HasLimit.mk (limitCone F) }
      -- see Note [lower instance priority]

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