Theorems · Theorem · functional analysis

lp.single_neg

∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), lp.single p i (-a) = -lp.single p i a

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupDecidableEq