noncomputable def AffineBuilding.aptDistGR {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (p q : DiscreteFibers.PointF ↑A) : ℝ

Distance between two points $p$, $q$ of the geometric realisation of an apartment, obtained by linearly extending the vertex distance using the barycentric weights of $p$ and $q$.

noncomputable def AffineBuilding.aptDistGR' {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (wtp wtq : V → ℝ) (σ τ : Finset V) : ℝ

Variant of aptDistGR taking weight functions and faces directly, useful for proofs that bypass the bundled PointF structure.

theorem AffineBuilding.buildingDist_wellDefined_via_iso_fix {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (v w : V) (hv₁ : ∃ s ∈ (↑A₁).faces, v ∈ s) (hw₁ : ∃ s ∈ (↑A₁).faces, w ∈ s) (hv₂ : ∃ s ∈ (↑A₂).faces, v ∈ s) (hw₂ : ∃ s ∈ (↑A₂).faces, w ∈ s) : md.dist_fn A₁ v w = md.dist_fn A₂ v w

Well-definedness of the building distance via the apartment-isomorphism / fix-of-intersection principle: the distance $d(v, w)$ measured inside any apartment containing both vertices is independent of the chosen apartment.

@[reducible, inline]

abbrev AffineBuilding.BuildingPointF {V : Type} [DecidableEq V] (b : Building V) : Type

A point of the geometric realisation of a building, abbreviating DiscreteFibers.PointF of the underlying simplicial complex.

def AffineBuilding.pointInApartment {V : Type} [DecidableEq V] (b : Building V) (p : BuildingPointF b) : Prop

A point of the building lies in some apartment if its supporting face is a face of one of the apartments of the system.