Theorem: Matroid.Flat.cl (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hF : M.Flat F
⊢ F ∈ {F_1 | M.Flat F_1 ∧ F ∩ M.E ⊆ F_1}
Tactic:
simpa
State after:
no goals