norm_eq_zero_iff

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.norm_eq_zero_iff

English

For any f in Lp with p > 0, the usual norm is zero iff f is the zero element.

Русский

Для любого f в Lp с p > 0 нормa равна нулю тогда, когда f есть ноль в пространстве.

LaTeX

$$$\forall f \in Lp\, E\, p\ μ\, (hp : 0 < p): \; \|f\| = 0 \iff f = 0$$$

Lean4

theorem norm_eq_zero_iff {f : Lp E p μ} (hp : 0 < p) : ‖f‖ = 0 ↔ f = 0 :=
  NNReal.coe_eq_zero.trans (nnnorm_eq_zero_iff hp)

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

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

Разделы

Аффилиация

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