structure GLnBuilding.PanelExtensionHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: every panel (codimension-$1$ face of a chamber) of an apartment frame $F$ extends in exactly two ways to a chamber, yielding the thin-apartment axiom for the $\mathrm{GL}_n$ building.

• extend (F : Frame k n) (panel : SubspaceFlag k n) : (∀ V ∈ panel.chain, Frame.IsCompatible k n F V) → panel.chain.length = n - 2 → ∃ (C₁ : SubspaceFlag k n) (C₂ : SubspaceFlag k n), IsChamber k n C₁ ∧ IsChamber k n C₂ ∧ C₁ ≠ C₂ ∧ (∀ V ∈ panel.chain, V ∈ C₁.chain) ∧ ∀ V ∈ panel.chain, V ∈ C₂.chain

noncomputable def GLnBuilding.thinApartmentHyp (k : Type u_1) [Field k] (n : ℕ) (h : PanelExtensionHyp k n) : ThinApartmentHyp k n

Converts a PanelExtensionHyp into the bundled ThinApartmentHyp consumed by the building construction.