Theorems · Theorem · combinatorics
Matroid.indep_iff_eRk_eq_encard_of_finite
∀ {α : Type u_1} {M : Matroid α} {I : Set α}, I.Finite → (M.Indep I ↔ M.eRk I = I.encard)- Defined in
- Mathlib.Combinatorics.Matroid.Rank.ENat
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- ENatstatement and proof · cited by 4,985
- le_reflproof · cited by 2,061
- Set.Finitestatement and proof · cited by 1,814
- Matroidstatement and proof · cited by 1,258
- Matroid.Indepstatement and proof · cited by 367
- Set.encardstatement and proof · cited by 327
- Matroid.eRkstatement and proof · cited by 101
- Matroid.IsBasis'proof · cited by 101
- Matroid.exists_isBasis'proof · cited by 30
- Matroid.IsBasis'.indepproof · cited by 27
- Matroid.IsBasis'.subsetproof · cited by 25
Cited by5
Results whose statement or proof uses this declaration.
- Matroid.eRk_lt_encard_of_dep_of_finiteproof · cited by 1
- Matroid.indep_iff_eRk_eq_encardproof · cited by 1
- Matroid.eRk_singleton_eq_one_iffproof · cited by 0
- Matroid.IsRkFinite.indep_of_encard_le_eRkproof · cited by 0
- Matroid.eRk_lt_encard_iff_dep_of_finiteproof · cited by 0