theorem isCompact_closure_image_of_isometry {X : Type u_1} [MetricSpace X] {f : X → X} (hf : Isometry f) {s : Set X} (hs : IsCompact (closure s)) : IsCompact (closure (f '' s))

If $f : X \to X$ is an isometry and the closure of $s$ is compact, then the closure of $f(s)$ is also compact.

def ActsByIsometries {E : Type u_1} [MetricSpace E] {W : Type u_2} (action : W → E → E) : Prop

The group action $W \to E \to E$ acts by isometries iff every element $w \in W$ acts as an isometry of the metric space $E$.

def orbitSet {E : Type u_1} {W : Type u_2} (action : W → E → E) (w : W) (S : Set E) : Set E

The image $w \cdot S$ of a subset $S \subseteq E$ under the action of $w \in W$.

theorem chamber_compact_closure {E : Type u_1} [MetricSpace E] {W : Type u_2} [Group W] {action : W → E → E} (hiso : ActsByIsometries action) {σ : Set E} (hσ : IsCompact (closure σ)) (w : W) : IsCompact (closure (orbitSet action w σ))

Chambers have compact closure under translation: if $\overline{\sigma}$ is compact then so is $\overline{w \cdot \sigma}$ for every $w \in W$ acting by isometries.

theorem chamber_isBounded {E : Type u_1} [MetricSpace E] {W : Type u_2} [Group W] {action : W → E → E} (hiso : ActsByIsometries action) {σ : Set E} (hσ : IsCompact (closure σ)) (w : W) : Bornology.IsBounded (orbitSet action w σ)

The image $w \cdot \sigma$ of a chamber with compact closure is bounded.

theorem chamber_diam_eq {E : Type u_1} [MetricSpace E] {W : Type u_2} [Group W] {action : W → E → E} (hiso : ActsByIsometries action) (σ : Set E) (w : W) : Metric.diam (orbitSet action w σ) = Metric.diam σ

Isometric translation preserves diameter: $\operatorname{diam}(w \cdot \sigma) = \operatorname{diam}(\sigma)$.