coe_ext

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ConcreteCategory.coe_ext

English

If the underlying functions of hom f and hom g are equal, then f = g.

Русский

Если базовые функции hom f и hom g равны, то f = g.

LaTeX

$$$\forall {X Y : C} {f g : X \to Y}, (coe (hom f) = coe (hom g)) \Rightarrow f = g$$$

Lean4

theorem coe_ext {X Y : C} {f g : X ⟶ Y} (h : ⇑(hom f) = ⇑(hom g)) : f = g :=
  ext (DFunLike.coe_injective h)

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

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

Разделы

Аффилиация

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