instIsClosedUnderIsomorphismsColimitsOfShape

Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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

English

The shape-colimit property P.colimitsOfShape J is closed under isomorphisms.

Русский

Свойство колимитов по форме J, примененное к P, is closed under isomorphisms.

LaTeX

$$$$ (P.colimitsOfShape(J)).IsClosedUnderIsomorphisms. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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