Commit 2024-12-09 09:39 b405b4d8

View on Github →

chore(Analysis/BoundedVariation): split file (#19784) Fixes #4862

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/BoundedVariation.lean

deleted theorem BoundedVariationOn.dist_le

deleted theorem BoundedVariationOn.locallyBoundedVariationOn

deleted theorem BoundedVariationOn.mono

deleted theorem BoundedVariationOn.sub_le

deleted def BoundedVariationOn

deleted theorem LipschitzOnWith.comp_boundedVariationOn

deleted theorem LipschitzOnWith.comp_eVariationOn_le

deleted theorem LipschitzOnWith.comp_locallyBoundedVariationOn

deleted theorem LipschitzOnWith.locallyBoundedVariationOn

deleted theorem LipschitzWith.comp_boundedVariationOn

deleted theorem LipschitzWith.comp_locallyBoundedVariationOn

deleted theorem LipschitzWith.locallyBoundedVariationOn

deleted theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

deleted def LocallyBoundedVariationOn

deleted theorem MonotoneOn.eVariationOn_le

deleted theorem MonotoneOn.locallyBoundedVariationOn

deleted theorem eVariationOn.Icc_add_Icc

deleted theorem eVariationOn.add_le_union

deleted theorem eVariationOn.add_point

deleted theorem eVariationOn.comp_eq_of_antitoneOn

deleted theorem eVariationOn.comp_eq_of_monotoneOn

deleted theorem eVariationOn.comp_inter_Icc_eq_of_monotoneOn

deleted theorem eVariationOn.comp_le_of_antitoneOn

deleted theorem eVariationOn.comp_le_of_monotoneOn

deleted theorem eVariationOn.comp_ofDual

deleted theorem eVariationOn.constant_on

deleted theorem eVariationOn.edist_le

deleted theorem eVariationOn.eq_of_edist_zero_on

deleted theorem eVariationOn.eq_of_eqOn

deleted theorem eVariationOn.eq_zero_iff

deleted theorem eVariationOn.lowerSemicontinuous_aux

deleted theorem eVariationOn.lowerSemicontinuous_uniformOn

deleted theorem eVariationOn.mono

deleted theorem eVariationOn.nonempty_monotone_mem

deleted theorem eVariationOn.sum_le

deleted theorem eVariationOn.sum_le_of_monotoneOn_Icc

deleted theorem eVariationOn.sum_le_of_monotoneOn_Iic

deleted theorem eVariationOn.union

Modified Mathlib/Analysis/ConstantSpeed.lean

Created Mathlib/Topology/EMetricSpace/BoundedVariation.lean

added theorem BoundedVariationOn.dist_le

added theorem BoundedVariationOn.locallyBoundedVariationOn

added theorem BoundedVariationOn.mono

added theorem BoundedVariationOn.sub_le

added def BoundedVariationOn

added theorem LipschitzOnWith.comp_boundedVariationOn

added theorem LipschitzOnWith.comp_eVariationOn_le

added theorem LipschitzOnWith.comp_locallyBoundedVariationOn

added theorem LipschitzOnWith.locallyBoundedVariationOn

added theorem LipschitzWith.comp_boundedVariationOn

added theorem LipschitzWith.comp_locallyBoundedVariationOn

added theorem LipschitzWith.locallyBoundedVariationOn

added theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

added def LocallyBoundedVariationOn

added theorem MonotoneOn.eVariationOn_le

added theorem MonotoneOn.locallyBoundedVariationOn

added theorem eVariationOn.Icc_add_Icc

added theorem eVariationOn.add_le_union

added theorem eVariationOn.add_point

added theorem eVariationOn.comp_eq_of_antitoneOn

added theorem eVariationOn.comp_eq_of_monotoneOn

added theorem eVariationOn.comp_inter_Icc_eq_of_monotoneOn

added theorem eVariationOn.comp_le_of_antitoneOn

added theorem eVariationOn.comp_le_of_monotoneOn

added theorem eVariationOn.comp_ofDual

added theorem eVariationOn.constant_on

added theorem eVariationOn.edist_le

added theorem eVariationOn.eq_of_edist_zero_on

added theorem eVariationOn.eq_of_eqOn

added theorem eVariationOn.eq_zero_iff

added theorem eVariationOn.lowerSemicontinuous_aux

added theorem eVariationOn.lowerSemicontinuous_uniformOn

added theorem eVariationOn.mono

added theorem eVariationOn.nonempty_monotone_mem

added theorem eVariationOn.sum_le

added theorem eVariationOn.sum_le_of_monotoneOn_Icc

added theorem eVariationOn.sum_le_of_monotoneOn_Iic

added theorem eVariationOn.union