instIsClosedUnderIsomorphisms — Mathlib

English

Let P be an object property on a category C that is closed under subobjects. Then P is closed under isomorphisms.

Русский

Пусть P — свойство объектов в категории C, замкнутое по подобъектам. Тогда P замкнуто по изоморфизмам.

LaTeX

$$$\forall {\mathcal C} [\mathbf{Category}(\mathcal C)], \forall P:\mathrm{ObjectProperty}(\mathcal C), \bigl(P.\IsClosedUnderSubobjects \Rightarrow P.\IsClosedUnderIsomorphisms\bigr).$$$

Lean4

instance : P.IsClosedUnderIsomorphisms where of_iso e := P.prop_of_mono e.inv

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