Mathlib Map

Theorems · Theorem · functional analysis

lp.single_add

∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a b : E i), lp.single p i (a + b) = lp.single p i a + lp.single p i b
Defined in
Mathlib.Analysis.Normed.Lp.lpSpace
Cited by
0 results in Mathlib
Foundations
Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroupDecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

lp.singleAddMonoidHom · cited by 2lp.singleAddMonoidHomNormedAddCommGroup · cited by 15752NormedAddCommGroupENNReal · cited by 9879ENNRealAddSubgroup · cited by 3232AddSubgroupPreLp · cited by 163PreLplp · cited by 157lplp.single · cited by 34lp.singlelp.ext · cited by 11lp.extPi.single_add · cited by 4Pi.single_addlp.single_addCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.