Theorems · Theorem · real analysis

eVariationOn.sum_le_of_monotoneOn_Icc

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α} {m n : ℕ}
  {u : ℕ → α},
  MonotoneOn u (Set.Icc m n) →
    (∀ i ∈ Set.Icc m n, u i ∈ s) → ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace