Theorems · Theorem · general topology

LipschitzOnWith.mul

∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x * g x) s

Defined in

Mathlib.Analysis.Normed.Group.Uniform

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedCommGroupPseudoEMetricSpace