instIsClosedUnderIsomorphismsLimitsOfShape

English

The limits-of-shape structure inherits closure under isomorphisms: if a limit exists for a diagram, an isomorphic diagram has a limit.

Русский

Пределы формы сохраняют замыкание по изоморфизмам: если существует предел для диаграммы, то для изоморфной диаграммы предел существует.

LaTeX

$$$(P.limitsOfShape J).IsClosedUnderIsomorphisms$$$

Lean4

instance : (P.limitsOfShape J).IsClosedUnderIsomorphisms where of_iso := by rintro _ _ e ⟨h⟩; exact ⟨h.ofIso e⟩

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