instHasLimitsOfSizeCondensedSet — Mathlib

English

The category of condensed sets has limits of all small diagrams; i.e., for every small diagram F, there exists a limit object Lim F in CondensedSet with the usual universal property.

Русский

Категория конденсированных множеств имеет пределы для всех малых диаграмм; то есть для каждой малой диаграммы F существует предел Lim F в CondensedSet, удовлетворяющий обычному универсальному свойству.

LaTeX

$$$\forall J\,\forall F\!:\, J \to \text{CondensedSet}, \exists L \in \text{CondensedSet}, \text{Lim}(F)=L \quad$ (existence of limits for all small diagrams).$$

Lean4

instance : HasLimitsOfSize.{u, u + 1} CondensedSet.{u} :=
  hasLimitsOfSizeShrink.{u, u + 1, u + 1, u} _

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