ext

Mathlib.Topology.Algebra.Algebra

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

English

An extensionality principle: two ContinuousAlgHoms are equal if they agree on all inputs.

Русский

Принцип экстенсивности: два ContinuousAlgHom равны, если для каждого входа они совпадают.

LaTeX

$$$\\text{ext}~{f,g} : (∀ x, f x = g x) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem ext {f g : A →A[R] B} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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

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

Разделы

Аффилиация

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