Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-24 14:38 9dca6f42

View on Github →

feat(topology/metric_space/lipschitz): add set.maps_to lemmas (#12266)

Estimated changes

Modified src/topology/metric_space/lipschitz.lean

modified theorem lipschitz_with.bounded_image

modified theorem lipschitz_with.diam_image_le

added theorem lipschitz_with.dist_le_mul_of_le

added theorem lipschitz_with.dist_lt_mul_of_lt

added theorem lipschitz_with.edist_le_mul_of_le

added theorem lipschitz_with.edist_lt_mul_of_lt

added theorem lipschitz_with.maps_to_ball

added theorem lipschitz_with.maps_to_closed_ball

added theorem lipschitz_with.maps_to_emetric_ball

added theorem lipschitz_with.maps_to_emetric_closed_ball

modified theorem lipschitz_with.nndist_le