Theorems · Definition · real analysis

variationOnFromTo

{α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → α → α → ℝ

The signed variation of f on the interval Icc a b intersected with the set s, squashed to a real (therefore only really meaningful if the variation is finite)

Defined in

Mathlib.Topology.EMetricSpace.VariationOnFromTo

Cited by

33 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace