English
For any c ∈ M and any set s ⊆ X, the diameter is preserved under the action: diam(c•s) = diam(s).
Русский
Для любого c ∈ M и любого множества s ⊆ X диагональ сохраняется под действием: diam(c•s) = diam(s).
LaTeX
$$$\operatorname{diam}(c\cdot s) = \operatorname{diam}(s)$$$
Lean4
@[to_additive (attr := simp)]
theorem diam_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) :
Metric.diam (c • s) = Metric.diam s :=
(isometry_smul _ _).diam_image s