isEquivalencePreservesLimits — Mathlib

English

If E is an equivalence, then E preserves limits of size; in particular, limits are preserved by E.

Русский

Если E — эквивалентность, она сохраняет пределы заданного размера; пределы сохраняются E.

LaTeX

$$$$ E \\text{ isEquivalence } \\Rightarrow \\mathrm{PreservesLimitsOfSize}(E). $$$$

Lean4

instance (priority := 100) isEquivalencePreservesLimits (E : D ⥤ C) [E.IsEquivalence] :
    PreservesLimitsOfSize.{v, u} E :=
  rightAdjoint_preservesLimits E.asEquivalence.symm.toAdjunction

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