reflectsLimitsOfSize_shrink — Mathlib

English

A statement that reflects limits of a large size can be shrunk to reflect limits of a smaller size.

Русский

Утверждение, отражающее пределы большого размера, можно сузить до отражения пределов меньшего размера.

LaTeX

$$$[\\mathrm{ReflectsLimitsOfSize}\\,(F)] \\Rightarrow [\\mathrm{ReflectsLimitsOfSize}\\,(F)]_{\\text{smaller}}$$$

Lean4

/-- `reflectsLimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsLimitsOfSize.{w w'} F`
from some other `reflectsLimitsOfSize F`.
-/
theorem reflectsLimitsOfSize_shrink (F : C ⥤ D) [ReflectsLimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsLimitsOfSize.{w, w'} F :=
  reflectsLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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