Theorems · Theorem · general topology

eHolderNorm_smul

∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  {α : Type u_3} [inst_2 : NormedRing α] [inst_3 : Module α Y] [NormSMulClass α Y] (c : α),
  eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Defined in

Mathlib.Topology.MetricSpace.HolderNorm

Cited by

2 results in Mathlib

Foundations

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

Assumes

MetricSpaceNormedAddCommGroupNormedRingModuleNormSMulClass