ext

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

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

English

A RingSeminorm p is zero if and only if p x = 0 for all x.

Русский

Норма RingSeminorm p равна нулю тогда и только тогда, когда p(x)=0 для всех x.

LaTeX

$$p = 0 ⇔ ∀ x, p x = 0$$

Lean4

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

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

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

Разделы

Аффилиация

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