Theorems · Definition · real analysis

LocallyBoundedVariationOn

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

A function has locally bounded variation on a set s if, given any interval [a, b] with endpoints in s, then the function has finite variation on s ∩ [a, b].

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

41 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace