eq_zero_iff

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

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

English

A RingSeminorm p equals zero if and only if for all x, p x equals zero.

Русский

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

LaTeX

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

Lean4

theorem eq_zero_iff {p : RingSeminorm R} : p = 0 ↔ ∀ x, p x = 0 :=
  DFunLike.ext_iff

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

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

Разделы

Аффилиация

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