instIsComonHomHom — Mathlib

English

Any morphism f: M ⟶ N in Comon C is automatically a comonoid homomorphism on its underlying morphism.

Русский

Любой морфизм f: M ⟶ N в Comon C автоматически является комоноидным гомоморфизмом на своем базовом гомоморфизме.

LaTeX

$$$\forall f: M \to N, \; IsComonHom(f.hom)$$$

Lean4

instance {M N : Comon C} (f : M ⟶ N) : IsComonHom f.hom :=
  inferInstanceAs (IsComonHom f.hom)

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