theorem ThicknessAptStructure.building_max_in_apt_is_apt_max {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} {pre : AptIsCoxeterProof.PreApartmentData K} {A : SimplicialComplex V} (hA : A ∈ pre.apartments) {C : Finset V} (hC_A : C ∈ A.faces) (hC_K : K.IsMaximal C) : A.IsMaximal C

A chamber of the building that lies in an apartment is also a maximal face of that apartment.

theorem ThicknessAptStructure.apt_max_is_building_max {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} {pre : AptIsCoxeterProof.PreApartmentData K} {A : SimplicialComplex V} (hA : A ∈ pre.apartments) {C : Finset V} (hC : A.IsMaximal C) : K.IsMaximal C

A maximal face of an apartment is also a chamber of the ambient building.