Theorems · Theorem · functional analysis

lp.single_smul

∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] [inst_4 : DecidableEq α] (p : ENNReal)
  (i : α) (c : 𝕜) (a : E i), lp.single p i (c • a) = c • lp.single p i a

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedRingModuleIsBoundedSMulDecidableEq