hasLimitsOfShape_of_equivalence — Mathlib

English

If J and J' are categories with an equivalence e: J ≌ J', and C has limits of shape J, then C has limits of shape J'.

Русский

Если две категории J и J' эквивалентны через эквивалентность e: J ≌ J', и в категории C существуют пределы формы J, то существуют пределы формы J'.

LaTeX

$$$\\text{HasLimitsOfShape}(J',C)$$$

Lean4

/-- We can transport limits of shape `J` along an equivalence `J ≌ J'`.
-/
theorem hasLimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J') [HasLimitsOfShape J C] :
    HasLimitsOfShape J' C := by
  constructor
  intro F
  apply hasLimit_of_equivalence_comp e

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