instIsClosedUnderIsomorphisms_1

Mathlib.CategoryTheory.ObjectProperty.EpiMono

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

English

If P is closed under quotients, then P is closed under isomorphisms.

Русский

Если P замкнуто по объёмам(quotients) — по квазиобразам, тогда P замкнуто по изоморфизмам.

LaTeX

$$$\forall C\, [\mathrm{Category}(C)],\ P.\IsClosedUnderQuotients \Rightarrow P.\IsClosedUnderIsomorphisms.$$$

Lean4

instance : P.IsClosedUnderIsomorphisms where of_iso e := P.prop_of_epi e.hom

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

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

Разделы

Аффилиация

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