def IsGalleryConvex {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (S : Set (Finset V)) : Prop

$S$ is gallery-convex in $K$ if every minimal gallery between two chambers of $S$ has all of its chambers in $S$.

def IsGate {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (S : Set (Finset V)) (C D : Finset V) : Prop

$D$ is a gate for chamber $C$ inside $S$ if $D \in S$ and $D$ minimizes the gallery distance from $C$ over chambers in $S$.

def IsConvexSubcomplex {V : Type u_1} [DecidableEq V] (K A : SimplicialComplex V) (_h : IsSubcomplex A K) : Prop

A subcomplex $A$ of $K$ is convex if its set of maximal chambers is gallery-convex in $K$.

theorem chain_exists_transition {α : Type u_2} {R : α → α → Prop} {a b : α} {l : List α} (hchain : List.IsChain R (a :: b :: l)) (P : α → Prop) (hPa : P a) (E : α) (hE_mem : E ∈ a :: b :: l) (hE_not : ¬P E) : ∃ (x : α) (y : α), x ∈ a :: b :: l ∧ y ∈ a :: b :: l ∧ R x y ∧ P x ∧ ¬P y

In a chain $a :: b :: l$ where $a$ satisfies $P$ but some element $E$ does not, there is an adjacent pair witnessing the $P$-to-$\lnot P$ transition.

theorem maximal_in_building_and_subcomplex {V : Type u_1} [DecidableEq V] (K A : SimplicialComplex V) (hAK : IsSubcomplex A K) (C : Finset V) (hC_A : C ∈ A.faces) (hC_K_max : K.IsMaximal C) : A.IsMaximal C

A face of $A$ that is maximal in $K$ is also maximal in $A$, when $A \subseteq K$.

theorem finset_image_eq_self_of_fixes {V : Type u_1} [DecidableEq V] {f : V → V} {s : Finset V} (hfix : ∀ v ∈ s, f v = v) : Finset.image f s = s

If $f$ fixes every element of a finset $s$, then $s.\mathrm{image}\, f = s$.

theorem Building.ApartmentsAreConvex {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (C D : Finset V), C ∈ A.faces → A.IsMaximal C → D ∈ A.faces → A.IsMaximal D → ∀ (g : Gallery b.toSimplicialComplex), g.Connects C D → g.length = galleryDist b.toSimplicialComplex C D → ∀ E ∈ g.chambers, E ∈ A.faces

Apartments in a building are gallery-convex: minimal galleries between chambers of an apartment $A$ stay inside $A$.

def ConvexHull {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C D : Finset V) : Set (Finset V)

Convex hull of two chambers $C, D$: the union of chambers occurring on some minimal gallery from $C$ to $D$.