rw [sUnion_eq_iUnion, biUnion_eq_iUnion, cl_iUnion_cl_eq_cl_iUnion]
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
Xs : Set (Set α)
⊢ M.cl (⋃ X ∈ Xs, M.cl X) = M.cl (⋃₀ Xs)
no goals