has_limits_of_equivalence — Mathlib

English

Let E: D ⥤ C be an equivalence and HasLimitsOfSize.{v,u} C. Then HasLimitsOfSize.{v,u} D holds.

Русский

Пусть E: D ⥤ C — эквивалентность и C имеет пределы размера {v,u}. Тогда D имеет пределы размера {v,u}.

LaTeX

$$$$(E\\; \\text{IsEquivalence}) \\land \\operatorname{HasLimitsOfSize}.{v,u}\\; C \\Rightarrow \\operatorname{HasLimitsOfSize}.{v,u}\\; D.$$$$

Lean4

/-- Transport a `HasLimitsOfSize` instance across an equivalence. -/
theorem has_limits_of_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfSize.{v, u} C] : HasLimitsOfSize.{v, u} D :=
  ⟨fun _ _ => hasLimitsOfShape_of_equivalence E⟩

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