theorem AptIsCoxeterProof.apt_face_in_chamber {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (s : Finset V) (hs : s ∈ A.faces) : ∃ (C : Finset V), A.IsMaximal C ∧ s ⊆ C

Every face of an apartment $A$ is contained in some maximal chamber of $A$.

theorem AptIsCoxeterProof.apt_gallery_connected {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : ∃ (g : Gallery A), g.chambers.head? = some C ∧ g.chambers.getLast? = some D

Any two maximal chambers of an apartment $A$ are connected by a gallery internal to $A$.

noncomputable def AptIsCoxeterProof.aptChamberComplex {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) : ChamberComplex V

The chamber complex structure on an apartment $A$ inherited from PreApartmentData.

theorem AptIsCoxeterProof.aptChamberComplex_eq {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) : (aptChamberComplex pre A hA).toSimplicialComplex = A

The simplicial complex underlying aptChamberComplex is precisely the apartment $A$.

theorem AptIsCoxeterProof.apt_is_thin {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) : (aptChamberComplex pre A hA).IsThin

The aptChamberComplex associated to an apartment is thin.

theorem AptIsCoxeterProof.apt_thinness_from_thickness {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (_hThick : K.IsThick) (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) : ∃ (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ cc.IsThin

In a thick chamber complex, every apartment admits an underlying thin chamber complex.