Commit 2026-08-18 19:45 fec8c8ef

View on Github →

feat: a bounded variation function is continuous off a countable set (#42841)

Estimated changes

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Modified Mathlib/Topology/EMetricSpace/VariationOnFromTo.lean

added theorem BoundedVariationOn.continuousAt_variationOnFromTo_iff

modified theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Iic

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_iff

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_inter_Ici

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_inter_Ici_iff

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_inter_Iic

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_inter_Iic_iff

added theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_leftLim_Iic

modified theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici

added theorem BoundedVariationOn.countable_not_continuousAt