Mathlib Map

Theorems · Definition · combinatorics

IndepMatroid.Indep

{α : Type u_2} → IndepMatroid α → Set α → Prop

The independence predicate

Defined in
Mathlib.Combinatorics.Matroid.IndepAxioms
Cited by
17 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IndepMatroid.matroid · cited by 4IndepMatroid.matroidIndepMatroid.ofFinset_indep · cited by 0IndepMatroid.ofFinset_ind…IndepMatroid.ofFinset_indep' · cited by 0IndepMatroid.ofFinset_ind…IndepMatroid.subset_ground · cited by 0IndepMatroid.subset_groundIndepMatroid.ofFinitary_indep · cited by 0IndepMatroid.ofFinitary_i…IndepMatroid.indep_aug · cited by 0IndepMatroid.indep_augIndepMatroid.indep_empty · cited by 0IndepMatroid.indep_emptyIndepMatroid.indep_maximal · cited by 0IndepMatroid.indep_maximalIndepMatroid.indep_subset · cited by 0IndepMatroid.indep_subsetMatroid.restrictIndepMatroid_Indep · cited by 0Matroid.restrictIndepMatr…IndepMatroid.matroid_Indep · cited by 0IndepMatroid.matroid_IndepIndepMatroid.matroid_IsBase · cited by 0IndepMatroid.matroid_IsBa…IndepMatroid.matroid_indep_iff · cited by 0IndepMatroid.matroid_inde…IndepMatroid.ofBddAugment_indep · cited by 0IndepMatroid.ofBddAugment…IndepMatroid.ofBdd_indep · cited by 0IndepMatroid.ofBdd_indepSet · cited by 53352SetIndepMatroid · cited by 15IndepMatroidIndepMatroid.IndepCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • IndepMatroidstatement and proof · cited by 15

Cited by18

Results whose statement or proof uses this declaration.