Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-24 12:44 bc91ed70

View on Github →

feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged (#18990)

Estimated changes

Modified src/analysis/normed/mul_action.lean

added theorem edist_smul_le

added theorem edist_smul₀

modified theorem lipschitz_with_smul

modified theorem nndist_smul₀

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/pointwise.lean

added theorem diam_smul₀

added theorem ediam_smul_le

added theorem ediam_smul₀

added theorem inf_dist_smul₀

added theorem inf_edist_smul₀

Modified src/data/real/ennreal.lean

modified theorem ennreal.mul_le_iff_le_inv

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem emetric.inf_edist_smul

Modified src/topology/metric_space/isometric_smul.lean

added theorem diam_smul

added theorem ediam_smul