English
If S is a bounded subset of a metric space X on which G acts by isometries, then for any g ∈ G the image g•S is bounded.
Русский
Если S — ограниченная подмножество метрического пространства X, на котором G действует изометрично, то его образ g•S под действием любого g ∈ G также ограничен.
LaTeX
$$$\text{IsBounded}(S) \Rightarrow \text{IsBounded}(c \cdot S),$$$
Lean4
/-- If `G` acts isometrically on `X`, then the image of a bounded set in `X` under scalar
multiplication by `c : G` is bounded. See also `Bornology.IsBounded.smul₀` for a similar lemma about
normed spaces. -/
@[to_additive /-- Given an additive isometric action of `G` on `X`, the image of a bounded set in
`X` under translation by `c : G` is bounded. -/
]
theorem smul [PseudoMetricSpace X] [SMul G X] [IsIsometricSMul G X] {s : Set X} (hs : IsBounded s) (c : G) :
IsBounded (c • s) :=
(isometry_smul X c).lipschitz.isBounded_image hs
