Documentation

Mathlib.Data.Matroid.Minor.Order

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, written N ≤m M, means that N = M ／ C ＼ D for some subset C and D of M.E.
Matroid.IsStrictMinor N M, written N <m M, means that N = M ／ C ＼ D for some subsets C and D of M.E that are not both nonempty.
Matroid.IsMinor.exists_eq_contract_delete_disjoint : we can choose C and D disjoint.

Minors #

def Matroid.IsMinor {α : Type u_1} (N M : Matroid α) :

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.

Equations

Instances For

def Matroid.«term_≤m_» :

Lean.TrailingParserDescr

≤m denotes the minor relation on matroids.

Equations

Instances For

@[simp]

theorem Matroid.contract_delete_isMinor {α : Type u_1} (M : Matroid α) (C D : Set α) :

(M.contract C).delete D ≤m M

theorem Matroid.IsMinor.exists_eq_contract_delete_disjoint {α : Type u_1} {M N : Matroid α} (h : N ≤m M) :

∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = (M.contract C).delete D

def Matroid.IsStrictMinor {α : Type u_1} (N M : Matroid α) :

N is a strict minor of M if N is a minor of M and N ≠ M. Equivalently, N is obtained from M by deleting/contracting subsets of the ground set that are not both empty.

Equations

Instances For

def Matroid.«term_<m_» :

Lean.TrailingParserDescr

<m denotes the strict minor relation on matroids.

Equations

Instances For

theorem Matroid.IsMinor.subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) :

N.E ⊆ M.E

theorem Matroid.IsMinor.refl {α : Type u_1} {M : Matroid α} :

M ≤m M

theorem Matroid.IsMinor.trans {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁ ≤m M₂) (h' : M₂ ≤m M₃) :

M₁ ≤m M₃

theorem Matroid.IsMinor.eq_of_ground_subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) (hE : M.E ⊆ N.E) :

M = N

theorem Matroid.IsMinor.antisymm {α : Type u_1} {M N : Matroid α} (h : N ≤m M) (h' : M ≤m N) :

N = M

instance Matroid.instPartialOrder (α : Type u_2) :

PartialOrder (Matroid α)

The minor order is a PartialOrder on Matroid α. We prefer the spelling N ≤m M over N ≤ M for the dot notation.

Equations

theorem Matroid.IsMinor.le {α : Type u_1} {M N : Matroid α} (h : N ≤m M) :

N ≤ M

theorem Matroid.IsStrictMinor.lt {α : Type u_1} {M N : Matroid α} (h : N <m M) :

N < M

@[simp]

theorem Matroid.le_eq_isMinor {α : Type u_1} :

(fun (M M' : Matroid α) => M ≤ M') = IsMinor

@[simp]

theorem Matroid.lt_eq_isStrictMinor {α : Type u_1} :

(fun (M M' : Matroid α) => M < M') = IsStrictMinor

theorem Matroid.isStrictMinor_iff_isMinor_ne {α : Type u_1} {M N : Matroid α} :

N <m M ↔ N ≤m M ∧ N ≠ M

theorem Matroid.IsStrictMinor.ne {α : Type u_1} {M N : Matroid α} (h : N <m M) :

N ≠ M

theorem Matroid.isStrictMinor_irrefl {α : Type u_1} (M : Matroid α) :

¬M <m M

theorem Matroid.IsStrictMinor.isMinor {α : Type u_1} {M N : Matroid α} (h : N <m M) :

N ≤m M

theorem Matroid.IsStrictMinor.not_isMinor {α : Type u_1} {M N : Matroid α} (h : N <m M) :

theorem Matroid.IsStrictMinor.ssubset {α : Type u_1} {M N : Matroid α} (h : N <m M) :

N.E ⊂ M.E

theorem Matroid.isStrictMinor_iff_isMinor_ssubset {α : Type u_1} {M N : Matroid α} :

N <m M ↔ N ≤m M ∧ N.E ⊂ M.E

theorem Matroid.IsStrictMinor.trans_isMinor {α : Type u_1} {M M' N : Matroid α} (h : N <m M) (h' : M ≤m M') :

N <m M'

theorem Matroid.IsMinor.trans_isStrictMinor {α : Type u_1} {M M' N : Matroid α} (h : N ≤m M) (h' : M <m M') :

N <m M'

theorem Matroid.IsStrictMinor.trans {α : Type u_1} {M M' N : Matroid α} (h : N <m M) (h' : M <m M') :

N <m M'

theorem Matroid.Indep.of_isMinor {α : Type u_1} {M N : Matroid α} {I : Set α} (hI : N.Indep I) (hNM : N ≤m M) :

theorem Matroid.IsNonloop.of_isMinor {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsNonloop e) (hNM : N ≤m M) :

theorem Matroid.Dep.of_isMinor {α : Type u_1} {M N : Matroid α} {D : Set α} (hD : M.Dep D) (hDN : D ⊆ N.E) (hNM : N ≤m M) :

N.Dep D

theorem Matroid.IsLoop.of_isMinor {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (heN : e ∈ N.E) (hNM : N ≤m M) :