Mathlib Map

Theorems · Definition · combinatorics

IndepMatroid.E

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

The ground set

Defined in
Mathlib.Combinatorics.Matroid.IndepAxioms
Cited by
11 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.indep_maximal · cited by 0IndepMatroid.indep_maximalMatroid.restrictIndepMatroid_E · cited by 0Matroid.restrictIndepMatr…IndepMatroid.matroid_E · cited by 0IndepMatroid.matroid_EIndepMatroid.subset_ground · cited by 0IndepMatroid.subset_groundIndepMatroid.ofBddAugment_E · cited by 0IndepMatroid.ofBddAugment…IndepMatroid.ofBdd_E · cited by 0IndepMatroid.ofBdd_EIndepMatroid.ofFinitaryCardAugment_E · cited by 0IndepMatroid.ofFinitaryCa…IndepMatroid.ofFinitary_E · cited by 0IndepMatroid.ofFinitary_EMatroid.dualIndepMatroid_E · cited by 0Matroid.dualIndepMatroid_EIndepMatroid.ofFinite_E · cited by 0IndepMatroid.ofFinite_EIndepMatroid.ofFinset_E · cited by 0IndepMatroid.ofFinset_ESet · cited by 53352SetIndepMatroid · cited by 15IndepMatroidIndepMatroid.ECITED 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 by12

Results whose statement or proof uses this declaration.