theorem GLnBuilding.finset_card_le_n {n : ℕ} (S : Finset (Fin n)) : S.card ≤ n

The cardinality of any Finset (Fin n) is at most $n$.

theorem GLnBuilding.finset_card_sdiff_sub {n : ℕ} {lower upper : Finset (Fin n)} (hsub : lower ⊆ upper) : (upper \ lower).card = upper.card - lower.card

$|U \setminus L| = |U| - |L|$ when $L \subseteq U$.

theorem GLnBuilding.chain_card_ge_succ {n : ℕ} {chain : List (Finset (Fin n))} (hpw : List.Pairwise (fun (x1 x2 : Finset (Fin n)) => x1 ⊂ x2) chain) (hne : ∀ S ∈ chain, S.Nonempty) (i : ℕ) (hi : i < chain.length) : i + 1 ≤ chain[i].card

In a strictly increasing chain of non-empty finsets, the $i$-th term has cardinality at least $i+1$.

theorem GLnBuilding.gap_filler_core {n : ℕ} (lower upper : Finset (Fin n)) (hsub : lower ⊆ upper) (hcard : 2 ≤ (upper \ lower).card) : ∃ (T₁ : Finset (Fin n)) (T₂ : Finset (Fin n)), T₁ ≠ T₂ ∧ T₁.Nonempty ∧ T₁ ≠ Finset.univ ∧ T₂.Nonempty ∧ T₂ ≠ Finset.univ ∧ lower ⊂ T₁ ∧ T₁ ⊂ upper ∧ lower ⊂ T₂ ∧ T₂ ⊂ upper

Core filler: if $|U \setminus L| \ge 2$, pick two distinct elements $a, b$ and form $L \cup \{a\}$, $L \cup \{b\}$, giving two distinct intermediate proper non-empty finsets.

theorem GLnBuilding.chain_elem_subset_of_lt {n : ℕ} {chain : List (Finset (Fin n))} (hpw : List.Pairwise (fun (x1 x2 : Finset (Fin n)) => x1 ⊂ x2) chain) {bound j : ℕ} (hj : j < chain.length) (hbound : bound < chain.length) (hjb : j ≤ bound) : chain[j] ⊆ chain[bound]

Earlier terms of a strictly-increasing chain are subsets of later terms.

noncomputable def GLnBuilding.finsetChainGapHyp (n : ℕ) (hn2 : 2 ≤ n) : FinsetChainGapHyp n

Proof of FinsetChainGapHyp: any length-$(n-2)$ chain of proper non-empty subsets of $\mathrm{Fin}\ n$ contains a position where two distinct insertions fit, by analysing where cardinalities first deviate from the "tight" pattern $|S_i| = i+1$.

noncomputable def GLnBuilding.extractFinset (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) (V : Submodule k (Vec k n)) : Finset (Fin n)

Extract the index set $S \subseteq \mathrm{Fin}\ n$ such that $V = \bigoplus_{i \in S} F.\mathrm{lines}\ i$ (via classical choice), or ∅ if no such $S$ exists.

theorem GLnBuilding.extractFinset_spec (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) (V : Submodule k (Vec k n)) (hcompat : Frame.IsCompatible k n F V) : V = ⨆ i ∈ extractFinset k n F V, F.lines i

For an $F$-compatible $V$, the extracted finset $S$ satisfies $V = \bigoplus_{i \in S} F.\mathrm{lines}\ i$.

theorem GLnBuilding.biSup_subset_le (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) (S₁ S₂ : Finset (Fin n)) (h : S₁ ⊆ S₂) : ⨆ i ∈ S₁, F.lines i ≤ ⨆ i ∈ S₂, F.lines i

$\bigoplus_{i \in S_1} L_i \le \bigoplus_{i \in S_2} L_i$ when $S_1 \subseteq S_2$.

theorem GLnBuilding.frame_line_not_le_biSup (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) (S₁ : Finset (Fin n)) {j : Fin n} (hj : j ∉ S₁) : ¬F.lines j ≤ ⨆ i ∈ S₁, F.lines i

If $j \notin S_1$, then $F.\mathrm{lines}\ j$ is not contained in $\bigoplus_{i \in S_1} L_i$, by the frame's independence.

theorem GLnBuilding.frame_biSup_ssubset (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) {S₁ S₂ : Finset (Fin n)} (h : S₁ ⊂ S₂) : ⨆ i ∈ S₁, F.lines i < ⨆ i ∈ S₂, F.lines i

Strict subset $S_1 \subsetneq S_2$ lifts to strict containment of frame-spans.

theorem GLnBuilding.frame_biSup_ne_bot (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) {S : Finset (Fin n)} (hne : S.Nonempty) : ⨆ i ∈ S, F.lines i ≠ ⊥

A non-empty index set $S$ produces a non-zero frame-span.

theorem GLnBuilding.frame_biSup_ne_top (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) {S : Finset (Fin n)} (hne : S ≠ Finset.univ) : ⨆ i ∈ S, F.lines i ≠ ⊤

A proper index set $S \ne \mathrm{Finset.univ}$ produces a proper frame-span.

theorem GLnBuilding.frame_biSup_injective (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) {S₁ S₂ : Finset (Fin n)} (hne : S₁ ≠ S₂) : ⨆ i ∈ S₁, F.lines i ≠ ⨆ i ∈ S₂, F.lines i

Distinct index sets produce distinct frame-spans (injectivity of $S \mapsto \bigoplus_{i \in S} L_i$).

noncomputable def GLnBuilding.frameFinsetCorrespondenceHyp (k : Type u_1) [Field k] (n : ℕ) : FrameFinsetCorrespondenceHyp k n

Proof of FrameFinsetCorrespondenceHyp: bundle the bijection between $F$-compatible subspaces and subsets of $\mathrm{Fin}\ n$ via extractFinset and $S \mapsto \bigoplus_{i \in S} L_i$.