Theorems · Theorem · measure theory

StieltjesFunction.length_subadditive_Icc_Ioo

∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R]
  [CompactIccSpace R] {a b : R} {c d : ℕ → R},
  Set.Icc a b ⊆ ⋃ i, Iotop (c i) (d i) → ENNReal.ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ENNReal.ofReal (↑f (d i) - ↑f (c i))

If a compact interval [a, b] is covered by a union of open interval (c i, d i), then f b - f a ≤ ∑ f (d i) - f (c i). This is an auxiliary technical statement to prove the same statement for half-open intervals, the point of the current statement being that one can use compactness to reduce it to a finite sum, and argue by induction on the size of the covering set. To be able to handle also the top element if there is one, we use Iotop instead of Ioo in the statement. As these intervals are all open, this does not change the proof.

Defined in

Mathlib.MeasureTheory.Measure.Stieltjes

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyCompactIccSpace