instIsClosedUnderIsomorphismsInd

Mathlib.CategoryTheory.ObjectProperty.Ind

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInd

English

Ind-ind: If P ≤ isFinitelyPresentable(C), then ind(ind(P)) = ind(P).

Русский

Ind-ind: если P ≤ isFinitelyPresentable(C), то ind(ind(P)) = ind(P).

LaTeX

$$$\text{If } P \leq \mathrm{isFinitelyPresentable}(C),\; \mathrm{ind}(\mathrm{ind}(P)) = \mathrm{ind}(P).$$$

Lean4

instance : P.ind.IsClosedUnderIsomorphisms where
  of_iso {X Y} e := fun ⟨J, _, _, pres, h⟩ ↦ ⟨J, ‹_›, ‹_›, pres.ofIso e, h⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru