ext

Mathlib.Order.Category.BddDistLat

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

English

Two morphisms with equal action on all elements are equal.

Русский

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

LaTeX

$$∀ X Y, ∀ f g: X ⟶ Y, ∀ x, f x = g x ⇒ f = g$$

Lean4

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

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

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

Разделы

Аффилиация

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