Theorems · Theorem · combinatorics
Matroid.sigma_isBasis_iff
∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I X : Set ((i : ι) × α i)},
(Matroid.sigma M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)- Defined in
- Mathlib.Combinatorics.Matroid.Sum
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
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
- Set.imageproof · cited by 5,609
- Set.preimagestatement and proof · cited by 4,946
- Set.univproof · cited by 3,945
- Matroidstatement and proof · cited by 1,258
- eq_or_neproof · cited by 1,117
- Matroid.Eproof · cited by 550
- LE.le.antisymmproof · cited by 507
- Matroid.Indepproof · cited by 367
- Matroid.IsBasisstatement · cited by 219
- Maximalproof · cited by 211
- Eq.subsetproof · cited by 124
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.