hasLimitsOfSizeShrink — Mathlib

English

From HasLimitsOfSize at a large size, one obtains HasLimitsOfSize at a smaller size via a universes comparison.

Русский

Из HasLimitsOfSize на большем размере следует HasLimitsOfSize на меньшем размере через сравнение вселенных.

LaTeX

$$$\\text{HasLimitsOfSize}(C)$$$

Lean4

/-- `hasLimitsOfSizeShrink.{v u} C` tries to obtain `HasLimitsOfSize.{v u} C`
from some other `HasLimitsOfSize C`.
-/
theorem hasLimitsOfSizeShrink [HasLimitsOfSize.{max v₁ v₂, max u₁ u₂} C] : HasLimitsOfSize.{v₁, u₁} C :=
  hasLimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

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