Theorems · Theorem · combinatorics

Matroid.Indep.notMem_closure_iff

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

Defined in: Mathlib.Combinatorics.Matroid.Closure
Cited by: 3 results in Mathlib
Foundations: Depth 86 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.

Cites9

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.subset_groundproof · cited by 61
Set.insert_subset_iffproof · cited by 35
Matroid.dep_iffproof · cited by 9
Matroid.Indep.mem_closure_iffproof · cited by 6

Cited by3

Results whose statement or proof uses this declaration.

Matroid.Indep.notMem_closure_iff_of_notMemproof · cited by 2
Matroid.IsBase.exchange_base_of_notMem_closureproof · cited by 1
Matroid.mem_closure_insertproof · cited by 1