Theorems · Theorem · combinatorics

Matroid.Indep.indep_insert_sdiff_of_mem_closure

∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep I → f ∈ M.closure I → e ∈ M.closure (insert f I \ {e}) → e ∈ insert f I → M.Indep (insert f I \ {e})

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

2 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound