English
For a scalar c ≠ 0, the diameter of the smoothed set c·sphere(x,r) equals |c| times the diameter of sphere(x,r).
Русский
Для c ≠ 0 диаметр множества c·сфера(x,r) равен |c| умножить на диаметр сферы(x,r).
LaTeX
$$$\operatorname{ediam}(c\cdot \mathrm{sphere}(x,r)) = \|c\|_+ \cdot \operatorname{ediam}(\mathrm{sphere}(x,r)).$$$
Lean4
theorem ediam_smul₀ (c : 𝕜) (s : Set E) : EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s :=
by
refine le_antisymm (ediam_smul_le c s) ?_
obtain rfl | hc := eq_or_ne c 0
· obtain rfl | hs := s.eq_empty_or_nonempty
· simp
simp [zero_smul_set hs, ← Set.singleton_zero]
· have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
