ext

Mathlib.ModelTheory.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Hom.ext

English

Two L-homomorphisms f,g: M →[L] N are equal if they agree on every input x ∈ M.

Русский

Два L-гомоморфизма f,g: M →[L] N равны, если они совпадают на каждом элементе x ∈ M.

LaTeX

$$$\\forall f,g:\\, M \\to[ L ] N,\\; (\\forall x:\\, M,\\; f\\,x = g\\,x) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem ext ⦃f g : M →[L] N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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

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

Разделы

Аффилиация

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