Theorems · Theorem · combinatorics
Matroid.ext_indep
∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁.E = M₂.E → (∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) → M₁ = M₂- Defined in
- Mathlib.Combinatorics.Matroid.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 65 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.Indepstatement and proof · cited by 367
- LE.le.trans_eqproof · cited by 328
- Maximalproof · cited by 211
- Matroid.Indep.subset_groundproof · cited by 61
- Matroid.ext_isBaseproof · cited by 7
Cited by15
Results whose statement or proof uses this declaration.
- Matroid.restrict_ground_eq_selfproof · cited by 10
- Matroid.restrict_restrict_eqproof · cited by 6
- Matroid.ext_iff_indepproof · cited by 3
- Matroid.ext_isCircuitproof · cited by 2
- Matroid.map_comapproof · cited by 1
- Matroid.ext_closureproof · cited by 1
- Matroid.contract_restrict_eq_restrict_contractproof · cited by 1
- Matroid.ext_indep_disjoint_loops_coloopsproof · cited by 0
- Matroid.ext_indep_iffproof · cited by 0
- Matroid.ext_isBase_indepproof · cited by 0
- Matroid.disjointSum_commproof · cited by 0
- Matroid.eq_of_restrictSubtype_eqproof · cited by 0