Mathlib Map

Theorems · Theorem · combinatorics

Matroid.Dep.subset_ground

∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D → D ⊆ M.E
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.IsCircuit.subset_ground · cited by 15IsCircuit.subset_groundMatroid.Dep.exists_isCircuit_subset · cited by 5Dep.exists_isCircuit_subs…Matroid.isCircuit_iff_dep_forall_sdiff_singleton_indep · cited by 3Matroid.isCircuit_iff_dep…Matroid.isCircuit_iff_forall_ssubset · cited by 0Matroid.isCircuit_iff_for…Matroid.IsRestriction.dep_iff · cited by 0IsRestriction.dep_iffMatroid.dep_iff_superset_isCircuit' · cited by 0Matroid.dep_iff_superset_…Matroid.Dep.of_contract · cited by 0Dep.of_contractSet · cited by 53352SetMatroid · cited by 1258MatroidMatroid.E · cited by 550Matroid.EMatroid.Dep · cited by 76Matroid.DepDep.subset_groundCITED 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.Estatement · cited by 550
  • Matroid.Depstatement and proof · cited by 76

Cited by7

Results whose statement or proof uses this declaration.