diam_smul — Mathlib

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

Похожие утверждения