Commit 2026-07-16 02:41 49ed1b2d

View on Github →

feat(Topology/EMetricSpace/BoundedVariation): more BoundedVariationOn and eVariationOn API (#41519) Various API for BoundedVariationOn and eVariationOn, including a formula for the eVariationOn for finite sets such as pairs, or the variation of the identity function, or more generally a monotone function.

Estimated changes

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

added theorem BoundedVariationOn.id_Icc

added theorem BoundedVariationOn.of_finite

modified theorem MonotoneOn.boundedVariationOn

added theorem MonotoneOn.eVariationOn_eq

modified theorem MonotoneOn.eVariationOn_le

modified theorem MonotoneOn.locallyBoundedVariationOn

added theorem eVariationOn.image_range_of_monotone

added theorem eVariationOn.pair

added theorem eVariationOn.union'

added theorem eVariationOn_id

added theorem eVariationOn_id_Icc