Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 19:34 5375918f

View on Github →

feat(topology/metric_space/antilipschitz): ediam of image/preimage (#8435) Also review API

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.div_le_of_le_mul'

added theorem ennreal.mul_le_of_le_div'

added theorem ennreal.mul_le_of_le_div

Modified src/data/real/nnreal.lean

added theorem nnreal.div_le_of_le_mul'

added theorem nnreal.div_le_of_le_mul

Modified src/topology/metric_space/antilipschitz.lean

added theorem antilipschitz_with.ediam_preimage_le

added theorem antilipschitz_with.le_mul_ediam_image

modified theorem antilipschitz_with.mul_le_dist

added theorem antilipschitz_with.mul_le_nndist

modified theorem antilipschitz_with_iff_le_mul_dist

added theorem antilipschitz_with_iff_le_mul_nndist