Theorems · Theorem · real analysis

MonotoneOn.eVariationOn_eq

∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α} {a b : α},
  MonotoneOn f s → a ∈ s → b ∈ s → eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)

The variation of a monotone real-valued function on s ∩ Icc a b equals its increment f b - f a.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

4 results in Mathlib

Foundations

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

Assumes

LinearOrder