uliftFunctor_preservesLimitsOfSize

English

The universe lift functor preserves limits of arbitrary size.

Русский

Функтор подъёма вселенной сохраняет пределы произвольного размера.

LaTeX

$$$\\text{uliftFunctorPreservesLimitsOfSize}$$$

Lean4

/-- The universe lift for groups preserves limits of arbitrary size.
-/
@[to_additive /-- The universe lift functor for additive groups preserves limits of arbitrary size. -/
    ]
noncomputable instance uliftFunctor_preservesLimitsOfSize : PreservesLimitsOfSize.{w', w} uliftFunctor.{v, u} where

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