ext

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

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

English

Extensionality principle for MulAlgebraNorm: equality of pointwise evaluations implies equality of norms.

Русский

Принцип экстенсиональности: совпадение по точечным значениям порождает равенство норм.

LaTeX

$$$\\forall p,q: MulAlgebraNorm\\,R\\,S, (\\forall x, p x = q x)\\to p=q$$$

Lean4

@[ext]
theorem ext {p q : MulAlgebraNorm R S} : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q

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

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

Разделы

Аффилиация

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