Theorems · Theorem · general topology

Bornology.IsBounded.vadd

∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd G X] [IsIsometricVAdd G X] {s : Set X},
  Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c +ᵥ s)

Given an additive isometric action of G on X, the image of a bounded set in X under translation by c : G is bounded.

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

PseudoMetricSpaceVAddIsIsometricVAdd