Theorems · Theorem · general topology

Bornology.IsBounded.smul

∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul G X] [IsIsometricSMul G X] {s : Set X},
  Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c • s)

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.

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

1 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceSMulIsIsometricSMul