eLpNorm_sub_comm — Mathlib

English

The Lp-norm of a difference is symmetric under swapping the operands: eLpNorm(f − g) p μ = eLpNorm(g − f) p μ.

Русский

Норма Lp для разности сохраняется при смене местами аргументов: eLpNorm(f − g) p μ = eLpNorm(g − f) p μ.

LaTeX

$$$eLpNorm(f - g)\\, p \\,\\mu = eLpNorm(g - f)\\, p \\,\\mu$$$

Lean4

theorem eLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) (μ : Measure α) : eLpNorm (f - g) p μ = eLpNorm (g - f) p μ := by
  simp [← eLpNorm_neg (f := f - g)]

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