def BornologyProp.pointOrbit {G : Type u_1} {X : Type u_2} (act : G → X → X) (E : Set G) (x : X) : Set X

Orbit of a point $x$ under the action of a set $E \subseteq G$: $\{g \cdot x : g \in E\}$.

def BornologyProp.setOrbit {G : Type u_1} {X : Type u_2} (act : G → X → X) (E : Set G) (Y : Set X) : Set X

Orbit of a set $Y \subseteq X$ under the action of $E \subseteq G$: $\{g \cdot y : g \in E, y \in Y\}$.

theorem BornologyProp.setOrbit_bounded_of_pointOrbit_bounded {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] (act : G → X → X) (hiso : ∀ (g : G) (a b : X), dist (act g a) (act g b) = dist a b) (E : Set G) (x : X) (Y : Set X) (hEx : Bornology.IsBounded (pointOrbit act E x)) (hY : Bornology.IsBounded Y) : Bornology.IsBounded (setOrbit act E Y)

If an isometric action has bounded point orbit at some $x$ and $Y$ is bounded, then the set orbit $E \cdot Y$ is bounded — by the triangle inequality.

theorem BornologyProp.bounded_orbit_of_finite_bruhat {G : Type u_3} [Group G] {X : Type u_4} [PseudoMetricSpace X] {B_idx : Type u_5} {M : CoxeterMatrix B_idx} {Ω : Type u_6} (bp : BNPair G M) (act : G → X → X) (hiso : ∀ (g : G) (a b : X), dist (act g a) (act g b) = dist a b) (extendedCells : Ω × M.Group → Set G) (E : Set G) (hE : BNPairBornology.IsBoundedGeneralized bp extendedCells E) : ∃ (x : X), Bornology.IsBounded (pointOrbit act E x)

Finite Bruhat coverage of $E$ implies the existence of a point with bounded orbit.

theorem BornologyProp.finite_bruhat_of_bounded_orbit_set {G : Type u_3} [Group G] {X : Type u_4} [PseudoMetricSpace X] {B_idx : Type u_5} {M : CoxeterMatrix B_idx} {Ω : Type u_6} (bp : BNPair G M) (act : G → X → X) (hiso : ∀ (g : G) (a b : X), dist (act g a) (act g b) = dist a b) (extendedCells : Ω × M.Group → Set G) (E : Set G) (hE : ∀ (Y : Set X), Bornology.IsBounded Y → Bornology.IsBounded (setOrbit act E Y)) : BNPairBornology.IsBoundedGeneralized bp extendedCells E

Conversely, if every set-orbit of bounded $Y$ is bounded, then $E$ is generalized BN-pair bounded.

theorem BornologyProp.proposition {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] {B_idx : Type u_3} {M : CoxeterMatrix B_idx} {Ω : Type u_4} (bp : BNPair G M) (act : G → X → X) (hiso : ∀ (g : G) (a b : X), dist (act g a) (act g b) = dist a b) (extendedCells : Ω × M.Group → Set G) (E : Set G) : BNPairBornology.IsBoundedGeneralized bp extendedCells E ↔ (∃ (x : X), Bornology.IsBounded (pointOrbit act E x)) ∧ ∀ (Y : Set X), Bornology.IsBounded Y → Bornology.IsBounded (setOrbit act E Y)

Main proposition (Section 17.7): $E$ is generalized BN-pair bounded $\iff$ some point orbit is bounded $\land$ every set orbit of a bounded set is bounded.

theorem BornologyProp.proposition_tfae {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] {B_idx : Type u_3} {M : CoxeterMatrix B_idx} {Ω : Type u_4} (bp : BNPair G M) (act : G → X → X) (hiso : ∀ (g : G) (a b : X), dist (act g a) (act g b) = dist a b) (extendedCells : Ω × M.Group → Set G) (E : Set G) : (BNPairBornology.IsBoundedGeneralized bp extendedCells E → ∃ (x : X), Bornology.IsBounded (pointOrbit act E x)) ∧ ((∃ (x : X), Bornology.IsBounded (pointOrbit act E x)) → ∀ (Y : Set X), Bornology.IsBounded Y → Bornology.IsBounded (setOrbit act E Y)) ∧ ((∀ (Y : Set X), Bornology.IsBounded Y → Bornology.IsBounded (setOrbit act E Y)) → BNPairBornology.IsBoundedGeneralized bp extendedCells E)

TFAE version of the main proposition presented as three implications forming a cycle.