Commit 2026-07-07 20:32 23b25044

View on Github →

chore: split BoundedVariation (#41421) Extract the part on variationOnFromTo. Otherwise, the file will get over the limit in a subsequent PR. This is a pure split, no material added or removed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/ConstantSpeed.lean

Modified Mathlib/MeasureTheory/VectorMeasure/BoundedVariation.lean

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

deleted theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici

deleted theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici

deleted theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn'

deleted theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

deleted theorem variationOnFromTo.abs_le_eVariationOn

deleted theorem variationOnFromTo.abs_sub_le_sub_of_le

deleted theorem variationOnFromTo.leftLim_eq

deleted theorem variationOnFromTo.rightLim_eq

deleted theorem variationOnFromTo.tendsto_left

deleted theorem variationOnFromTo.tendsto_right

Created Mathlib/Topology/EMetricSpace/VariationOnFromTo.lean

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici

added theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn'

added theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

added theorem variationOnFromTo.abs_le_eVariationOn

added theorem variationOnFromTo.abs_sub_le_sub_of_le

added theorem variationOnFromTo.leftLim_eq

added theorem variationOnFromTo.rightLim_eq

added theorem variationOnFromTo.tendsto_left

added theorem variationOnFromTo.tendsto_right