ediam_smul_le — Mathlib

English

Scaling by a nonzero scalar c multiplies the (Euclidean) diameter of a set by |c|; more precisely, ediam(c·s) = |c| · ediam(s).

Русский

Умножение множителя c на множество s масштабирует его диаметр на |c|: ediam(c·s) = |c| · ediam(s).

LaTeX

$$$\operatorname{ediam}(c\cdot s) = \|c\|_+ \cdot \operatorname{ediam}(s).$$$

Lean4

theorem ediam_smul_le (c : 𝕜) (s : Set E) : EMetric.diam (c • s) ≤ ‖c‖₊ • EMetric.diam s :=
  (lipschitzWith_smul c).ediam_image_le s

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