instIsComonHomComp — Mathlib

English

If f: M → N and g: N → O are comonoid morphisms, then their composite f ≫ g is also a comonoid morphism.

Русский

Если f: M → N и g: N → O являются морфизмами комоноидов, то их композиция f ≫ g также является морфизмом комоноида.

LaTeX

$$$\forall f: M \to N, g: N \to O$, if $f$ and $g$ are comonoid morphisms, then $f \;\circ\; g$ is a comonoid morphism.$$

Lean4

instance (f : M ⟶ N) (g : N ⟶ O) [IsComonHom f] [IsComonHom g] : IsComonHom (f ≫ g) where

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