Commit 2026-06-29 11:32 8857f7aa

View on Github →

feat: more results on bounded variation functions (#41099)

Estimated changes

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

added theorem BoundedVariationOn.eVariationOn_Ici_eq_Ioi_add_edist

added theorem BoundedVariationOn.eVariationOn_Iic_eq_Iio_add_edist

deleted theorem BoundedVariationOn.ofDual

added theorem BoundedVariationOn.tendsto_eVariationOn_Icc_left

added theorem BoundedVariationOn.tendsto_eVariationOn_Icc_right

added theorem LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_left

added theorem LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_right

added theorem MonotoneOn.boundedVariationOn

added theorem eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt'

added theorem eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt

added theorem eVariationOn.eVariationOn_Ioc_eq_Icc_of_continuousWithinAt'

added theorem eVariationOn.eVariationOn_Ioc_eq_Icc_of_continuousWithinAt

modified theorem eVariationOn.eVariationOn_leftLim_le

added theorem eVariationOn.eVariationOn_on_inter_Ici_eq_Ioi_add_edist

added theorem eVariationOn.eVariationOn_on_inter_Iic_eq_Iio_add_edist

modified theorem eVariationOn.eVariationOn_rightLim_le

added theorem eVariationOn.eq_biSup_inter_Icc

added theorem eVariationOn.locallyBoundedVariation_ofDual

added theorem variationOnFromTo.leftLim_eq

added theorem variationOnFromTo.rightLim_eq

added theorem variationOnFromTo.tendsto_left

added theorem variationOnFromTo.tendsto_right