norm_exponent_zero — Mathlib

English

Let f be an element of the Lp space with exponent p = 0. Then the Lp-norm of f is zero: ||f|| = 0.

Русский

Пусть f принадлежит пространству Lp при показателе p = 0. Тогда Lp-норма f равна нулю: ||f|| = 0.

LaTeX

$$$\forall f \in Lp\, E\, p\, μ:\; \|f\| = 0$, где $p = 0$.$$

Lean4

@[simp]
theorem norm_exponent_zero (f : Lp E 0 μ) : ‖f‖ = 0 := by
  -- Squeezed for performance reasons
  simp only [norm_def, eLpNorm_exponent_zero, ENNReal.toReal_zero]

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