hasLimitsOfSize_skeleton — Mathlib

English

If C has limits of size {w, w'}, then Skeleton(C) has limits of size {w, w'}.

Русский

Если у C есть пределы размера {w, w'}, то у Skeleton(C) есть пределы того же размера.

LaTeX

$$$\\forall \\{w,w'\\}, \\ HasLimitsOfSize{\\{w, w'\\}}\, C \\Rightarrow HasLimitsOfSize{\\{w, w'\\}}\\,(\\mathrm{Skeleton}\\;C)$$$

Lean4

instance hasLimitsOfSize_skeleton [HasLimitsOfSize.{w, w'} C] : HasLimitsOfSize.{w, w'} (Skeleton C) :=
  hasLimits_of_hasLimits_createsLimits (fromSkeleton C)

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