simpa
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ ∀ (i : ↑(range Fs)), M.Basis ((fun F => ↑F) i ∩ B) ((fun F => ↑F) i)
no goals