Commit 2023-05-25 12:49 ff68ab1c

View on Github →

feat: forward-port PR 18990 (#4328) Forward-port of leanprover-community/mathlib#18990 Original title: feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged

Estimated changes

Modified Mathlib/Analysis/Normed/MulAction.lean

added theorem edist_smul_le

added theorem edist_smul₀

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

added theorem diam_smul₀

added theorem ediam_smul_le

added theorem ediam_smul₀

added theorem infDist_smul₀

added theorem infEdist_smul₀

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem EMetric.infEdist_smul

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

added theorem diam_smul

added theorem ediam_smul