Theorems · Theorem · combinatorics

Matroid.Indep.notMem_closure_iff_of_notMem

∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α},
  M.Indep I →
    e ∉ I →
      autoParam (e ∈ M.E) Matroid.Indep.notMem_closure_iff_of_notMem._auto_1 → (e ∉ M.closure I ↔ M.Indep (insert e I))

Defined in: Mathlib.Combinatorics.Matroid.Closure
Cited by: 2 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Matroidstatement and proof · cited by 1,258
Matroid.Estatement and proof · cited by 550
Matroid.Indepstatement and proof · cited by 367
Matroid.closurestatement · cited by 272
Matroid.Indep.notMem_closure_iffproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subsetproof · cited by 3
Matroid.IsColoop.insert_indep_of_indepproof · cited by 0