Theorems · Theorem · general topology

LipschitzWith.sub

∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x - g x

Defined in

Mathlib.Analysis.Normed.Group.Uniform

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupPseudoEMetricSpace