structure AffineBuilding.SimplexAtInfinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Type

An ideal simplex of the building at infinity: a nonempty set of points at infinity that arises as a subset of $S_\infty$ for some sector $S$ (Section 16.8).

• points : Set (PointAtInfinity b md)
• from_sector : ∃ (S : Sector b), self.points ⊆ S.pointsAtInfinity md
• nonempty : self.points.Nonempty

structure AffineBuilding.ApartmentAtInfinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Type

An apartment $A_\infty$ of the building at infinity: the boundary of a Euclidean apartment $A \subseteq X$, packaged with its ideal simplices (Section 16.8).

• apartment : SimplicialComplex V
• apartment_mem : self.apartment ∈ b.apartmentSystem.apartments
• simplices : Set (SimplexAtInfinity b md)
• simplices_from_apartment (σ : SimplexAtInfinity b md) : σ ∈ self.simplices → ∃ (S : Sector b), S.apartment = self.apartment

structure AffineBuilding.BuildingAtInfinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Type

The building at infinity $X_\infty$ of an affine building $X$: ideal simplices together with apartments $A_\infty$, satisfying the building axiom that any two simplices lie in a common apartment (Sections 16.8–16.9).

• simplices : Set (SimplexAtInfinity b md)
• apartments : Set (ApartmentAtInfinity b md)
• apartment_simplices_mem (A : ApartmentAtInfinity b md) : A ∈ self.apartments → A.simplices ⊆ self.simplices
• contains_pair (σ₁ : SimplexAtInfinity b md) : σ₁ ∈ self.simplices → ∀ σ₂ ∈ self.simplices, ∃ A ∈ self.apartments, σ₁ ∈ A.simplices ∧ σ₂ ∈ A.simplices

def AffineBuilding.BuildingAtInfinity.IsSpherical {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (Binf : BuildingAtInfinity b md) : Prop

The building at infinity is spherical: each apartment $A_\infty$ has finitely many simplices and at least one apartment exists (Section 16.10).