instIsComonHomInv — Mathlib

English

If f: M → N is a comonoid morphism and an isomorphism, then its inverse f^{-1} is also a comonoid morphism.

Русский

Если f: M → N — комоноидный морфизм и изоморфизм, то его обратный f^{-1} также является комоноидным морфизмом.

LaTeX

$$$\forall f: M \to N, IsComonHom(f) \land IsIso(f) \Rightarrow IsComonHom(f^{-1}).$$$

Lean4

instance (f : M ⟶ N) [IsComonHom f] [IsIso f] : IsComonHom (inv f) where

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