hasLimitsOfSize — Mathlib

English

In the small setting, the limit cone is given by Shrink(F.sections) and a projection map defined via an equivalence with F.sections.

Русский

В малой размерности предел конуса задается Shrink(F.sections) и отображением проекций через эквиваленцию с F.sections.

LaTeX

$$$\\mathrm{limitCone} : \\mathrm{Cone}(F) \\quad (\\text{with } \\mathrm{pt}=\\mathrm{Shrink}(F.\\mathrmsections) )$ and $\\pi_j(u) = ((\\mathrm{equivShrink } F.\\mathrmsections).symm\, u).val_j$$$

Lean4

/-- The category of types has all limits.

More specifically, when `UnivLE.{v, u}`, the category `Type u` has all `v`-small limits. -/
@[stacks 002U]
instance (priority := 1300) hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} (Type u) where
  has_limits_of_shape _ := { }

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