Theorems · Theorem · real analysis

eVariationOn.comp_eq_of_monotoneOn

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {t : Set β} (φ : β → α),
  MonotoneOn φ t → eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceLinearOrder