hasLimit_comp_equivalence — Mathlib

English

If E is an equivalence and HasLimit (K ⋙ E), then HasLimit K.

Русский

Если E — эквивалентность и HasLimit(K ∘ E), тогда HasLimit K.

LaTeX

$$$$ \\text{HasLimit}(K) \\Leftarrow \\text{HasLimit}(K \\circ E) \\text{ for equivalence } E. $$$$

Lean4

theorem hasLimit_comp_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimit K] : HasLimit (K ⋙ E) :=
  HasLimit.mk
    { cone := E.mapCone (limit.cone K)
      isLimit := isLimitOfPreserves _ (limit.isLimit K) }

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