theorem IsometryBuilding.standardApartments_simplices_eq {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (A₁ : Apartment B n) (hA₁ : A₁ ∈ standardApartments B n) (A₂ : Apartment B n) (hA₂ : A₂ ∈ standardApartments B n) : A₁.simplices = A₂.simplices

Helper: in the isometry building, all standard apartments share the same set of simplices (namely, all isotropic chains).

noncomputable def IsometryBuilding.apartmentExchangeHypInstance {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : ApartmentExchangeHyp B n

Apartment exchange axiom for the isometry building: any two apartments sharing a chamber admit a bijection of simplices fixing the common ones. The identity works because all standard apartments coincide as simplicial sets.