Mathlib v3 is deprecated. Go to Mathlib v4

Theorem antilipschitz_with.le_mul_ediam_image

Modification history

2021-07-27 19:34

src/topology/metric_space/antilipschitz.lean

feat(topology/metric_space/antilipschitz): ediam of image/preimage (#8435) …

Added antilipschitz_with.le_mul_ediam_image View on Github →