limit_eq_iInf — Mathlib

English

For any diagram F: J ⥤ α into a complete lattice α, its limit equals the infimum of the image of J, i.e., lim F = ∧_{j ∈ J} F(j).

Русский

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

LaTeX

$$$\\forall {J} [\\mathsf{Category} J]\\, (F: J \\to α), \\; \\operatorname{limit} F = \\inf (F\\.obj).$$$

Lean4

/-- The limit of a functor into a complete lattice is the infimum of the objects in the image.
-/
theorem limit_eq_iInf (F : J ⥤ α) : limit F = iInf F.obj :=
  (IsLimit.conePointUniqueUpToIso (limit.isLimit F) (limitCone F).isLimit).to_eq

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