∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f g : X → Y},
  MemHolder r f → MemHolder r g → nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g