2026-06-08 11:39
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
feat: a bounded variation function is the difference of two monotone functions that add up to the variation (#40289) …
Added LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn'