Theorems · Theorem · real analysis

LipschitzOnWith.comp_boundedVariationOn

∀ {α : 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 → BoundedVariationOn g s → BoundedVariationOn (f ∘ g) s

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpacePseudoEMetricSpace