simp [extension]
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
I : Set α
⊢ (C.extension e).Indep I ↔ M.Indep I ∨ e ∈ I \ M.E ∧ M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C
no goals