Theorems · Theorem · real analysis

eVariationOn.sum_le

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

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

6 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace