Commit 2023-11-08 08:49 b4636030

View on Github →

chore(Lipschitz): split (#8264) Move parts that don't need MetricSpaces to a new file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/EMetricSpace/Lipschitz.lean

added theorem LipschitzOnWith.ediam_image2_le

added theorem LipschitzOnWith.edist_le_mul_of_le

added theorem LipschitzOnWith.edist_lt_of_edist_lt_div

added theorem LipschitzOnWith.mono

added def LipschitzOnWith

added theorem LipschitzWith.comp_lipschitzOnWith

added theorem LipschitzWith.ediam_image_le

added theorem LipschitzWith.edist_iterate_succ_le_geometric

added theorem LipschitzWith.edist_le_mul

added theorem LipschitzWith.edist_le_mul_of_le

added theorem LipschitzWith.edist_lt_mul_of_lt

added theorem LipschitzWith.edist_lt_of_edist_lt_div

added theorem LipschitzWith.edist_lt_top

added theorem LipschitzWith.mapsTo_emetric_ball

added theorem LipschitzWith.mapsTo_emetric_closedBall

added theorem LipschitzWith.mul_edist_le

added theorem LipschitzWith.subtype_mk

added def LipschitzWith

added def LocallyLipschitz

added theorem MapsTo.lipschitzOnWith_iff_restrict

added theorem continuousOn_prod_of_continuousOn_lipschitzOnWith

added theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith

added theorem continuous_prod_of_continuous_lipschitzWith

added theorem continuous_prod_of_dense_continuous_lipschitzWith

added theorem lipschitzOnWith_empty

added theorem lipschitzOnWith_iff_restrict

added theorem lipschitzOn_univ

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

deleted theorem LipschitzOnWith.ediam_image2_le

deleted theorem LipschitzOnWith.edist_le_mul_of_le

deleted theorem LipschitzOnWith.edist_lt_of_edist_lt_div

modified theorem LipschitzOnWith.extend_pi

modified theorem LipschitzOnWith.extend_real

deleted theorem LipschitzOnWith.mono

deleted def LipschitzOnWith

deleted theorem LipschitzWith.comp_lipschitzOnWith

deleted theorem LipschitzWith.ediam_image_le

deleted theorem LipschitzWith.edist_iterate_succ_le_geometric

deleted theorem LipschitzWith.edist_le_mul

deleted theorem LipschitzWith.edist_le_mul_of_le

deleted theorem LipschitzWith.edist_lt_mul_of_lt

deleted theorem LipschitzWith.edist_lt_of_edist_lt_div

deleted theorem LipschitzWith.edist_lt_top

deleted theorem LipschitzWith.mapsTo_emetric_ball

deleted theorem LipschitzWith.mapsTo_emetric_closedBall

deleted theorem LipschitzWith.mul_edist_le

deleted theorem LipschitzWith.subtype_mk

deleted def LipschitzWith

deleted def LocallyLipschitz

deleted theorem MapsTo.lipschitzOnWith_iff_restrict

modified theorem continuousAt_of_locally_lipschitz

deleted theorem continuousOn_prod_of_continuousOn_lipschitzOnWith

deleted theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith

deleted theorem continuous_prod_of_continuous_lipschitzWith

deleted theorem continuous_prod_of_dense_continuous_lipschitzWith

deleted theorem lipschitzOnWith_empty

deleted theorem lipschitzOnWith_iff_restrict

deleted theorem lipschitzOn_univ