Commit 2023-03-06 08:57 aeba075b

View on Github →

feat: port Topology.MetricSpace.Lipschitz (#2634)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Lipschitz.lean

added theorem LipschitzOnWith.edist_lt_of_edist_lt_div

added theorem LipschitzOnWith.extend_pi

added theorem LipschitzOnWith.extend_real

added theorem LipschitzOnWith.mono

added def LipschitzOnWith

added theorem LipschitzWith.bounded_image

added theorem LipschitzWith.coe_toLocallyBoundedMap

added theorem LipschitzWith.comap_cobounded_le

added theorem LipschitzWith.comp_lipschitzOnWith

added theorem LipschitzWith.const_max

added theorem LipschitzWith.const_min

added theorem LipschitzWith.diam_image_le

added theorem LipschitzWith.dist_iterate_succ_le_geometric

added theorem LipschitzWith.dist_le_mul_of_le

added theorem LipschitzWith.dist_lt_mul_of_lt

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_ball

added theorem LipschitzWith.mapsTo_closedBall

added theorem LipschitzWith.mapsTo_emetric_ball

added theorem LipschitzWith.mapsTo_emetric_closedBall

added theorem LipschitzWith.max_const

added theorem LipschitzWith.min_const

added theorem LipschitzWith.mul_edist_le

added theorem LipschitzWith.nndist_le

added theorem LipschitzWith.subtype_mk

added def LipschitzWith.toLocallyBoundedMap

added def LipschitzWith

added theorem MapsTo.lipschitzOnWith_iff_restrict

added theorem Metric.Bounded.left_of_prod

added theorem Metric.Bounded.right_of_prod

added theorem Metric.bounded_prod

added theorem Metric.bounded_prod_of_nonempty

added theorem continuousAt_of_locally_lipschitz

added theorem continuousOn_prod_of_continuousOn_lipschitz_on

added theorem continuous_prod_of_continuous_lipschitz

added theorem lipschitzOnWith_empty

added theorem lipschitzOnWith_iff_dist_le_mul

added theorem lipschitzOnWith_iff_restrict

added theorem lipschitzWith_iff_dist_le_mul

added theorem lipschitzWith_max

added theorem lipschitzWith_min

added theorem lipschitz_on_univ