ediam_smul — Mathlib

English

Diameter is preserved under an isometric SMul action: ediam(c•s) = ediam(s) for any c.

Русский

Диаметр множества сохраняется при изометрическом действии: ediam(c•s) = ediam(s).

LaTeX

$$$\mathrm{ediam}(c\cdot s) = \mathrm{ediam}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem ediam_smul [SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) : EMetric.diam (c • s) = EMetric.diam s :=
  (isometry_smul _ _).ediam_image s

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