ext

Mathlib.CategoryTheory.Monoidal.Comon_

URI: https://scilib.ai/kg/mathlib#Comon.ext

English

Two morphisms of comonoids are equal if their underlying arrows are equal.

Русский

Две морфизмы комоноидов равны, если их базовые стрелы равны.

LaTeX

$$$\forall X Y:\ Comon C,\; \forall f,g: X ⟶ Y,\; f.hom = g.hom \Rightarrow f = g$$$

Lean4

@[ext]
theorem ext {X Y : Comon C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g :=
  Hom.ext w

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru