Theorems · Theorem · combinatorics

Matroid.Indep.insert_sdiff_indep_iff

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

This can be used for rewriting if the LHS is inside a binder and it is unknown whether f = e.

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

2 results in Mathlib

Foundations

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