Theorems · Theorem · real analysis

eVariationOn.add_le_union

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α},
  (∀ x ∈ s, ∀ y ∈ t, x ≤ y) → eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

The variation of a function on the union of two sets s and t, with s to the left of t, bounds the sum of the variations along s and 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

LinearOrderPseudoEMetricSpace