Theorems · Theorem · real analysis

eVariationOn.add_point

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

Consider a monotone function u parameterizing some points of a set s. Given x ∈ s, then one can find another monotone function v parameterizing the same points as u, with x added. In particular, the variation of a function along u is bounded by its variation along v.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace