theorem AffineBuilding.chamber_sector_common_apartment_thm {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (C : Finset V) (hC : b.IsMaximal C) (S : Sector b) : ∃ A ∈ b.apartmentSystem.apartments, C ∈ A.faces ∧ ∃ (S' : Sector b), Sector.Subsector b S' S ∧ SetInApartment A S'.vertices

Wrapper exporting the chamber-and-sector common-apartment axiom from SectorInfrastructure.

theorem AffineBuilding.simplex_image_eq_of_fixes {V : Type} [DecidableEq V] {K L : SimplicialComplex V} (φ : SimplicialMap K L) (s : Finset V) (hfix : ∀ v ∈ s, φ.toFun v = v) : Finset.image φ.toFun s = s

A simplicial map that fixes a simplex pointwise leaves its image equal to itself.

theorem AffineBuilding.face_in_codomain_of_fixes {V : Type} [DecidableEq V] {K L : SimplicialComplex V} (φ : SimplicialMap K L) (s : Finset V) (hs : s ∈ K.faces) (hfix : ∀ v ∈ s, φ.toFun v = v) : s ∈ L.faces

If a simplicial map fixes a simplex pointwise, the simplex lies in the codomain complex.

theorem AffineBuilding.image_ssubset_of_ssubset_of_injective {V : Type} [DecidableEq V] {K L : SimplicialComplex V} (φ : SimplicialMap K L) (hinj : Function.Injective φ.toFun) {s t : Finset V} (hs : s ∈ K.faces) (ht : t ∈ K.faces) (hst : s ⊂ t) : Finset.image φ.toFun s ⊂ Finset.image φ.toFun t

Strict inclusion of simplices is preserved by the image under an injective map.

def AffineBuilding.IsVertexOf {V : Type} [DecidableEq V] (K : SimplicialComplex V) (v : V) : Prop

Predicate: $v$ is a vertex of $K$ (lies in some face).