Theorems · Theorem · combinatorics

Matroid.IsBase.isBase_insert_sdiff_of_mem_closure

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

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

2 results in Mathlib

Foundations

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