Theorems · Theorem · combinatorics
Matroid.isBase_restrict_iff
∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
autoParam (X ⊆ M.E) Matroid.isBase_restrict_iff._auto_1 → ((M.restrict X).IsBase I ↔ M.IsBasis I X)- Cited by
- 11 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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 and proof · cited by 550
- Matroid.Indepproof · cited by 367
- Matroid.IsBasestatement · cited by 239
- Matroid.IsBasisstatement and proof · cited by 219
- Maximalproof · cited by 211
- Matroid.restrictstatement and proof · cited by 111
Cited by11
Results whose statement or proof uses this declaration.
- Matroid.IsBasis.restrict_isBaseproof · cited by 2
- Matroid.delete_isBase_iffproof · cited by 2
- Matroid.IsBasis.isBasis_restrict_of_subsetproof · cited by 1
- Matroid.IsBasis.eq_exchange_of_sdiff_eq_singletonproof · cited by 1
- Matroid.IsBasis.exchangeproof · cited by 1
- Matroid.IsBase.isBasis_of_isRestrictionproof · cited by 1
- Matroid.IsBasis.transferproof · cited by 1
- Matroid.Indep.contract_isBase_iffproof · cited by 1
- Matroid.IsBasis.isBase_restrictproof · cited by 1
- Matroid.Indep.exists_insert_of_not_isBasisproof · cited by 0
- Matroid.Indep.exists_isBasis_subset_union_isBasisproof · cited by 0