hasLimitsOfSize — Mathlib

English

If D has limits of a certain size, then the category of J-sheaves has limits of the same size.

Русский

Если D имеет пределы заданного размера, то у шейфов J D есть пределы такого же размера.

LaTeX

$$$(\text{HasLimitsOfSize } {u_1,u_2} D) \Rightarrow (\text{HasLimitsOfSize } {u_1,u_2} (\mathrm{Sh}(J,D))).$$$

Lean4

instance hasLimitsOfSize [HasLimitsOfSize.{u₁, u₂} D] : HasLimitsOfSize.{u₁, u₂} (Sheaf J D) :=
  hasLimits_of_hasLimits_createsLimits (sheafToPresheaf J D)

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