instIsClosedUnderIsomorphismsUnopOfOpposite

English

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

Русский

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

LaTeX

$$$P.IsClosedUnderIsomorphisms \Rightarrow P.unop.IsClosedUnderIsomorphisms$$$

Lean4

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

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