Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lipschitz_with.dist_le_mul_of_le

Modification history

2022-02-24 14:38

src/topology/metric_space/lipschitz.lean

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

Added lipschitz_with.dist_le_mul_of_le View on Github →