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

Hypothesis: any finite list of proper non-zero subspaces is simultaneously compatible with some frame $F$ — i.e.\ admits a simultaneous adapted basis.

• adapt (subs : List (Submodule k (Vec k n))) : (∀ V ∈ subs, V ≠ ⊥ ∧ V ≠ ⊤) → ∃ (F : Frame k n), ∀ V ∈ subs, Frame.IsCompatible k n F V

noncomputable def GLnBuilding.simultaneousRefinementOfAdapted (k : Type u_1) [Field k] (n : ℕ) (h : AdaptedBasisHyp k n) : SimultaneousRefinementHyp k n

Wrap AdaptedBasisHyp as a SimultaneousRefinementHyp — they are the same property phrased identically.