Matroid Minors #
A matroid N = M / C \ D
obtained from a matroid M
by a contraction then a delete,
(or equivalently, by any number of contractions/deletions in any order) is a minor of M
.
This gives a partial order on Matroid α
that is ubiquitous in matroid theory,
and interacts nicely with duality and linear representations.
Although we provide a PartialOrder
instance on Matroid α
corresponding to the minor order,
we do not use the M ≤ N
/ N < M
notation directly,
instead writing N ≤m M
and N <m M
for more convenient dot notation.
Main Declarations #
Matroid.IsMinor N M
, writtenN ≤m M
, means thatN = M / C \ D
for some subsetC
andD
ofM.E
.Matroid.IsStrictMinor N M
, writtenN <m M
, means thatN = M / C \ D
for some subsetsC
andD
ofM.E
that are not both nonempty.Matroid.IsMinor.exists_eq_contract_delete_disjoint
: we can chooseC
andD
disjoint.
Minors #
N
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.
Instances For
≤m
denotes the minor relation on matroids.
Equations
- Matroid.«term_≤m_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤m_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤m ") (Lean.ParserDescr.cat `term 51))
Instances For
<m
denotes the strict minor relation on matroids.
Equations
- Matroid.«term_<m_» = Lean.ParserDescr.trailingNode `Matroid.«term_<m_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <m ") (Lean.ParserDescr.cat `term 51))
Instances For
The minor order is a PartialOrder
on Matroid α
.
We prefer the spelling N ≤m M
over N ≤ M
for the dot notation.