Theorems · Theorem · functional analysis

WithLp.prod_norm_eq_add

∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : Norm α] [inst_1 : Norm β],
  0 < p.toReal → ∀ (f : WithLp p (α × β)), ‖f‖ = (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ p.toReal) ^ (1 / p.toReal)

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

6 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormNorm