hom_ext — Mathlib

English

For two morphisms between commutative comonoids, equality on the underlying morphisms implies equality of the comonoid morphisms.

Русский

Для двух морфизмов между комоноидами равенство подлежащих морфизмов порождает равенство самих морфизмов комоноидов.

LaTeX

$$$\\forall A,B : \\text{CommComon } C, \\; f,g : A \\to B, \\; f.hom = g.hom \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {A B : CommComon C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
  Comon.Hom.ext h

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