theorem galleryDist_le_of_gallery {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (g : Gallery K) (hconn : g.Connects C D) : galleryDist K C D ≤ g.length

A gallery connecting $C$ to $D$ gives an upper bound for $d(C, D)$.

theorem exists_retraction_gallery {V : Type u_1} [DecidableEq V] {b : Building V} (ρ : BuildingRetraction b) (L : List (Finset V)) (hne : L ≠ []) (hmax : ∀ C ∈ L, b.IsMaximal C) (hchain : List.IsChain b.Adjacent L) : ∃ (g : Gallery ρ.apt), g.Connects (Finset.image ρ.map (L.head hne)) (Finset.image ρ.map (L.getLast hne)) ∧ g.length ≤ L.length - 1

The retraction $\rho$ maps each gallery in the building to a (possibly shorter) gallery in the apartment $\rho.apt$ connecting the images of the endpoints.

theorem retraction_image_gallery_bound {V : Type u_1} [DecidableEq V] {b : Building V} (ρ : BuildingRetraction b) (g : Gallery b.toSimplicialComplex) {C D : Finset V} (hconn : g.Connects C D) : galleryDist ρ.apt (Finset.image ρ.map C) (Finset.image ρ.map D) ≤ g.length

The apartment-distance of $\rho(C), \rho(D)$ is bounded above by the length of any gallery from $C$ to $D$ in the building.

theorem BuildingRetraction.isDistanceDiminishing {V : Type u_1} [DecidableEq V] {b : Building V} (ρ : BuildingRetraction b) : ρ.IsDistanceDiminishing

Every building retraction $\rho : X \to A$ is distance-diminishing: $d_A(\rho(C), \rho(D)) \le d_X(C, D)$ for all chambers $C, D$.