hasLimit_iff_of_iso — Mathlib

English

For any two functors F, G related by an isomorphism α, HasLimit F holds if and only if HasLimit G holds.

Русский

Для двух функторов F и G, связанных изоморфизмом α, имеет место: предел существует для F тогда и только тогда, когда существует предел для G.

LaTeX

$$$\\mathrm{HasLimit}(F) \\iff \\mathrm{HasLimit}(G)$$$

Lean4

theorem hasLimit_iff_of_iso {F G : J ⥤ C} (α : F ≅ G) : HasLimit F ↔ HasLimit G :=
  ⟨fun _ ↦ hasLimit_of_iso α, fun _ ↦ hasLimit_of_iso α.symm⟩
    -- See the construction of limits from products and equalizers
    -- for an example usage.

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