Mathlib Map

Theorems · Theorem · combinatorics

Matroid.Indep.not_dep

∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ¬M.Dep I
Defined in
Mathlib.Combinatorics.Matroid.Basic
Cited by
7 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matroid.Dep.superset · cited by 6Dep.supersetMatroid.Dep.exists_isCircuit_subset · cited by 5Dep.exists_isCircuit_subs…Matroid.Indep.insert_dep_iff · cited by 4Indep.insert_dep_iffMatroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset · cited by 3Indep.closure_sInter_eq_b…Matroid.mem_closure_insert · cited by 1Matroid.mem_closure_insertMatroid.eRk_lt_encard_of_dep_of_finite · cited by 1Matroid.eRk_lt_encard_of_…Matroid.isCircuit_iff_forall_ssubset · cited by 0Matroid.isCircuit_iff_for…Set · cited by 53352SetMatroid · cited by 1258MatroidMatroid.Indep · cited by 367Matroid.IndepMatroid.Dep · cited by 76Matroid.DepIndep.not_depCITED BYCITES

Cites4

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.Indepstatement and proof · cited by 367
  • Matroid.Depstatement and proof · cited by 76

Cited by7

Results whose statement or proof uses this declaration.