def GLnBuilding.sigmaWitness {n : ℕ} (i : Fin (n + 1)) : Finset (Fin n)

The set of indices $\{j : j < i\}$ used to assemble $V_i$ from the first $i$ frame lines.

theorem GLnBuilding.card_sigmaWitness_eq {n : ℕ} (i : Fin (n + 1)) : (sigmaWitness i).card = ↑i

The cardinality of sigmaWitness i is $i$.

theorem GLnBuilding.gapVector_mem_of_lt {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (j : Fin n) (i : Fin (n + 1)) (hjlt : ↑j < ↑i) : hσ.gapVector j ∈ σ.spaces i

If $j < i$ then the $j$-th gap vector of a strict flag lies in $V_i$.

theorem GLnBuilding.finrank_biSup_span_singleton_eq_card {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] {ι : Type u_3} [Fintype ι] {v : ι → M} (hli : LinearIndependent k v) (S : Finset ι) : Module.finrank k ↥(⨆ i ∈ S, k ∙ v i) = S.card

For a linearly independent family $\{v_i\}$ and a finite subset $S$, the dimension of $\bigvee_{i \in S} k \cdot v_i$ equals $|S|$.

theorem GLnBuilding.biSup_span_singleton_eq_of_le_of_finrank {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] {ι : Type u_3} [Fintype ι] {v : ι → M} (hli : LinearIndependent k v) (S : Finset ι) (W : Submodule k M) [FiniteDimensional k ↥W] (hle : ⨆ i ∈ S, k ∙ v i ≤ W) (hfr : Module.finrank k ↥W = S.card) : ⨆ i ∈ S, k ∙ v i = W

Equality criterion: $\bigvee_{i \in S} k \cdot v_i = W$ whenever the left side is contained in $W$ and their dimensions agree.

theorem GLnBuilding.refinementFrame_sigma_eq {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) [FiniteDimensional k (Vec k n)] (i : Fin (n + 1)) : ⨆ j ∈ sigmaWitness i, (refinementFrame hσ).lines j = σ.spaces i

Refinement compatibility: each subspace $V_i$ of a strict flag $\sigma$ is reconstructed from the refinement frame as $V_i = \bigvee_{j < i} (\text{frame line } j)$.