ext

Mathlib.Order.Category.BddOrd

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

English

Two morphisms in BddOrd are equal if they agree on every element.

Русский

Две морфизмы в BddOrd равны, если согласованы на каждом элементе.

LaTeX

$$∀ {X Y : BddOrd} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g$$

Lean4

@[ext]
theorem ext {X Y : BddOrd} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
  ConcreteCategory.hom_ext _ _ w

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

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

Разделы

Аффилиация

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