simpa
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
ι : Type u_3
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ?m.45300.Indep (⋃ i, (fun i => I ↑i) i)
no goals