Theorems · Theorem · general topology

HolderWith.add

∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : SeminormedAddCommGroup Y] {C C' r : NNReal}
  {f g : X → Y}, HolderWith C r f → HolderWith C' r g → HolderWith (C + C') r (f + g)

Defined in

Mathlib.Topology.MetricSpace.Holder

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSeminormedAddCommGroup