instIsClosedUnderIsomorphismsOppositeOp

English

If P is closed under isomorphisms, then P.op is closed under isomorphisms as well.

Русский

Если P замкнуто относительно изоморфизмов, то и P.op замкнуто относительно изоморфизмов.

LaTeX

$$$P \text{ is closed under isomorphisms } \Rightarrow P^{\mathrm{op}}.\text{IsClosedUnderIsomorphisms}$$$

Lean4

instance (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.op.IsClosedUnderIsomorphisms where
  of_iso e hX := P.prop_of_iso e.symm.unop hX

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