Theorems · Theorem · real analysis

LipschitzOnWith.comp_eVariationOn_le

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E},
  LipschitzOnWith C f t → ∀ {g : α → E} {s : Set α}, Set.MapsTo g s t → eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpacePseudoEMetricSpace