theorem PropositionRetractionProperties.boundedSubsets_iff_exists_orbit_bounded {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (ctx : FixedPointSubgroups.BuildingGroupContext Gt B_idx M) (E : Set Gt) : ctx.born.isBounded E ↔ ∃ (x : ctx.X), Bornology.IsBounded (FixedPointSubgroups.orbitSet ctx.action E x)

A subset $E \subseteq G$ is bounded in the building-bornology if and only if there exists some $x \in X$ whose $E$-orbit is bounded in the apartment.

theorem PropositionRetractionProperties.boundedSubsets_iff_forall_action_bounded {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (ctx : FixedPointSubgroups.BuildingGroupContext Gt B_idx M) (E : Set Gt) : ctx.born.isBounded E ↔ ∀ (Y : Set ctx.X), Bornology.IsBounded Y → Bornology.IsBounded (FixedPointSubgroups.actionOnSet ctx.action E Y)

A subset $E \subseteq G$ is bounded in the bornology iff its action sends every bounded subset $Y \subseteq X$ to a bounded subset.

theorem PropositionRetractionProperties.exists_orbit_bounded_iff_forall_action_bounded {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (ctx : FixedPointSubgroups.BuildingGroupContext Gt B_idx M) (E : Set Gt) : (∃ (x : ctx.X), Bornology.IsBounded (FixedPointSubgroups.orbitSet ctx.action E x)) ↔ ∀ (Y : Set ctx.X), Bornology.IsBounded Y → Bornology.IsBounded (FixedPointSubgroups.actionOnSet ctx.action E Y)

There exists some $x \in X$ with bounded orbit iff every bounded subset of $X$ has bounded image under $E$.

theorem PropositionRetractionProperties.stabilizer_born_bounded_iff_orbit_bounded {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (ctx : FixedPointSubgroups.BuildingGroupContext Gt B_idx M) (x : ctx.X) : ctx.born.isBounded ↑(FixedPointSubgroups.pointStabilizer ctx.action x) ↔ Bornology.IsBounded (FixedPointSubgroups.orbitSet ctx.action (↑(FixedPointSubgroups.pointStabilizer ctx.action x)) x)

The point stabilizer of $x$ is bounded in the bornology iff its orbit at $x$ is bounded.

theorem PropositionRetractionProperties.boundedSubsets_G_iff_orbit_bounded {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (ctx : FixedPointSubgroups.BuildingGroupContext Gt B_idx M) (E : Set Gt) (hE_in_G : E ⊆ ↑ctx.gbnpair.G) : ctx.born.isBounded E ↔ ∃ (x : ctx.X), Bornology.IsBounded (FixedPointSubgroups.orbitSet ctx.action E x)

For subsets contained in $G$, the bornology bound is equivalent to the existence of a bounded orbit.