def CombinatorialGeometry.IsGateConvexInApartment {V : Type u_1} [DecidableEq V] (K A : SimplicialComplex V) (σ : Set (Finset V)) : Prop

$\sigma$ is gate-convex in apartment $A$ if its chambers are maximal in $A$ and every maximal chamber $D$ of $A$ has a gate inside $\sigma$.

def CombinatorialGeometry.IsHalfApartment {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (_A : SimplicialComplex V) (H : Set (Finset V)) : Prop

A half-apartment of $K$ is the set of fixed chambers of some folding $f$.

structure CombinatorialGeometry.GateConvexHypotheses {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : Prop

Hypotheses asserting that every gate-convex subset of an apartment is a fixed-chamber set of some folding strictly avoiding a chosen outside chamber $D$.

• folding_from_gate (σ : Set (Finset V)) : IsGateConvexInApartment b.toSimplicialComplex A σ → ∀ (D : Finset V), A.IsMaximal D → D ∉ σ → ∃ (K_A : ChamberComplex V) (_ : K_A.toSimplicialComplex = A) (f : K_A.Folding), (∀ C ∈ σ, C ∈ f.fixedChambers) ∧ D ∉ f.fixedChambers