∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] (c : 𝕜) (s : Set E), Metric.ediam (c • s) = ‖c‖₊ • Metric.ediam s