Theorem: Matroid.modularSet_iff (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
M : Matroid α
X : Set α
⊢ M.ModularSet X ↔ ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Tactic:
simp [ModularSet, modularPair_iff]
State after:
no goals