Mathlib Map

Theorems · Theorem · combinatorics

Matroid.IsBasis.subset

∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → I ⊆ X
Defined in
Mathlib.Combinatorics.Matroid.Basic
Cited by
45 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.IsBasis.closure_eq_closure · cited by 13IsBasis.closure_eq_closureMatroid.Indep.closure_eq_setOfPred_isBasis_insert · cited by 6Indep.closure_eq_setOfPre…Matroid.IsBasis.map · cited by 6IsBasis.mapMatroid.Dep.exists_isCircuit_subset · cited by 5Dep.exists_isCircuit_subs…Matroid.Indep.eq_of_isBasis · cited by 4Indep.eq_of_isBasisMatroid.IsBasis.insert_dep · cited by 3IsBasis.insert_depMatroid.indep_iff_forall_notMem_closure_sdiff · cited by 3Matroid.indep_iff_forall_…Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset · cited by 3Indep.closure_sInter_eq_b…Matroid.IsBasis.contract_eq_contract_delete · cited by 3IsBasis.contract_eq_contr…Matroid.IsBasis.exists_isBasis_inter_eq_of_superset · cited by 2IsBasis.exists_isBasis_in…Matroid.IsBasis.iUnion_isBasis_iUnion · cited by 2IsBasis.iUnion_isBasis_iU…Matroid.comap_isBasis_iff · cited by 2Matroid.comap_isBasis_iffMatroid.isBasis_iff_indep_closure · cited by 2Matroid.isBasis_iff_indep…Matroid.Spanning.isBase_restrict_iff · cited by 2Spanning.isBase_restrict_…Matroid.IsCircuit.isBasis_iff_eq_sdiff_singleton · cited by 2IsCircuit.isBasis_iff_eq_…Set · cited by 53352SetMatroid · cited by 1258MatroidMatroid.IsBasis · cited by 219Matroid.IsBasisIsBasis.subsetCITED BYCITES

Cites3

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.IsBasisstatement and proof · cited by 219

Cited by45

Results whose statement or proof uses this declaration.