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 #

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

    ≤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

        <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

          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) :
          ¬M ≤m N
          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) :
          M.Indep I
          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) :
          N.IsLoop e