def SimplicialComplex.chambers {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) : Set (Finset V)

The set of chambers (maximal faces) of a simplicial complex $K$.

def Building.IsSpherical {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

A building is spherical if every apartment has finitely many faces (equivalently, finite diameter).

noncomputable def SimplicialComplex.diameter {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) : ℕ

The diameter of a simplicial complex: the supremum of gallery distances between pairs of chambers.

def AreOpposite {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C D : Finset V) : Prop

Two chambers $C, D$ of $K$ are opposite if both are chambers and their gallery distance is maximal among all pairs of chambers in $K$.

theorem areOpposite_symm {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (h : AreOpposite K C D) : AreOpposite K D C

The opposition relation between chambers is symmetric.

theorem SimplicialComplex.mem_chambers_iff {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C : Finset V) : C ∈ K.chambers ↔ K.IsMaximal C

Membership in K.chambers is the same as being a maximal face.

theorem SimplicialComplex.chambers_subset_faces {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) : K.chambers ⊆ K.faces

Every chamber is a face.

theorem Building.IsSpherical.finite_chambers {V : Type u_1} [DecidableEq V] (b : Building V) (hsph : b.IsSpherical) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : A.chambers.Finite

In a spherical building, each apartment has finitely many chambers.