smul₀ — Mathlib

English

The infimum diameter under smul by c equals the smul of the infimum diameter: ediam(c·s) = ||c||·ediam(s).

Русский

Инфинумный диаметр сохраняется под умножением: ediam(c·s) = ||c||·ediam(s).

LaTeX

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

Lean4

/-- Image of a bounded set in a normed space under scalar multiplication by a constant is
bounded. See also `Bornology.IsBounded.smul` for a similar lemma about an isometric action. -/
theorem smul₀ {s : Set E} (hs : IsBounded s) (c : 𝕜) : IsBounded (c • s) :=
  (lipschitzWith_smul c).isBounded_image hs

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