Mathlib v3 is deprecated. Go to Mathlib v4

Theorem antilipschitz_with.ediam_preimage_le

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.ediam_preimage_le View on Github →