ext

Mathlib.Order.Hom.Basic

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

English

Two OrderHom maps are equal if their underlying functions are equal.

Русский

Два отображения OrderHom равны, если равны их базовые функции.

LaTeX

$$$\\forall f,g:\\alpha \\to_o \\beta,\\ (f:α→β)=(g) \\Rightarrow f=g$.$$

Lean4

@[ext]
theorem ext (f g : α →o β) (h : (f : α → β) = g) : f = g :=
  DFunLike.coe_injective h

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

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

Разделы

Аффилиация

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