Theorems · Theorem · general topology

LocallyLipschitzOn.add

∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s g → LocallyLipschitzOn s fun x => f x + g x

Defined in

Mathlib.Analysis.Normed.Group.Uniform

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupPseudoEMetricSpace