hasLimitsOfSizeOfUnivLE — Mathlib

English

A category that has larger limits also has smaller limits; limits transfer along universe level embeddings.

Русский

Категория, в которой существуют большие пределы, обладает также меньшими пределами; пределы переносятся через вложения уровней ВС.

LaTeX

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

Lean4

/-- A category that has larger limits also has smaller limits. -/
theorem hasLimitsOfSizeOfUnivLE [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasLimitsOfSize.{v₁, u₁} C] :
    HasLimitsOfSize.{v₂, u₂} C where
  has_limits_of_shape J
    {_} := hasLimitsOfShape_of_equivalence ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

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