single_sub — Mathlib

English

For a finite index set s and f, the p-real power of the norm of the sum of single terms equals the sum of p-real powers of norms.

Русский

Для конечного множества индексов s и функции f сумма норм через single имеет выражение через сумму норм в степенях p.

LaTeX

$$$\|\sum_{i\in s} \text{lp.single } p i (f_i)\|^{p^{\mathbb{R}}} = \sum_{i\in s} \|f_i\|^{p^{\mathbb{R}}}.$$$

Lean4

@[simp]
protected theorem single_sub (p) (i : α) (a b : E i) : lp.single p i (a - b) = lp.single p i a - lp.single p i b :=
  ext <| Pi.single_sub _ _ _

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