Theorems · Theorem · combinatorics

Matroid.indep_iff_forall_notMem_closure_sdiff

∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_notMem_closure_sdiff._auto_1 →
    (M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e}))

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

Cites18

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 and proof · cited by 272
Matroid.IsBasisproof · cited by 219
Set.sdiff_subsetproof · cited by 156
Eq.subsetproof · cited by 124
LE.le.antisymm'proof · cited by 104
by_contraproof · cited by 60
Matroid.IsBasis.indepproof · cited by 51
Matroid.IsBasis.subsetproof · cited by 45

Cited by3

Results whose statement or proof uses this declaration.

Matroid.indep_iff_forall_notMem_closure_sdiff'proof · cited by 3
Matroid.indep_iff_forall_closure_ssubset_of_ssubsetproof · cited by 0
Matroid.indep_iff_forall_notMem_closure_diffproof · cited by 0