hasLimit_of_equivalence_comp — Mathlib

English

Same as above, restated for a separate instance.

Русский

То же самое, переформулировано для другого примера.

LaTeX

$$$\\mathrm{HasLimit}(e.functor ⋙ F)$$$

Lean4

/-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
-/
theorem hasLimit_of_equivalence_comp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F :=
  by
  haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
  apply hasLimit_of_iso (e.invFunIdAssoc F)

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