Theorems · Definition · combinatorics
Matroid.IsMinor
{α : Type u_1} → Matroid α → Matroid α → PropN is a minor of M if N = M ／ C ＼ D for some C and D.
The definition itself does not require C and D to be disjoint,
or even to be subsets of the ground set. See Matroid.IsMinor.exists_eq_contract_delete_disjoint
for the fact that we can choose C and D with these properties.
- Cited by
- 19 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Matroidstatement and proof · cited by 1,258
- Matroid.contractproof · cited by 103
- Matroid.deleteproof · cited by 86
Cited by20
Results whose statement or proof uses this declaration.
- Matroid.IsStrictMinorproof · cited by 12
- Matroid.IsMinor.eq_of_ground_subsetstatement and proof · cited by 2
- Matroid.IsMinor.subsetstatement and proof · cited by 2
- Matroid.IsStrictMinor.isMinorstatement · cited by 2
- Matroid.IsMinor.antisymmstatement and proof · cited by 1
- Matroid.IsMinor.lestatement and proof · cited by 1
- Matroid.Indep.of_isMinorstatement and proof · cited by 1
- Matroid.Dep.of_isMinorstatement and proof · cited by 1
- Matroid.IsLoop.of_isMinorstatement and proof · cited by 0
- Matroid.IsMinor.exists_eq_contract_delete_disjointstatement and proof · cited by 0
- Matroid.IsMinor.reflstatement · cited by 0
- Matroid.IsMinor.transstatement and proof · cited by 0