Documentation

Mathlib.Data.Matroid.Constructions

Some constructions of matroids #

This file defines some very elementary examples of matroids, namely those with at most one base.

Main definitions #

For E : Set α, ...

Implementation details #

To avoid the tedious process of certifying the matroid axioms for each of these easy examples, we bootstrap the definitions starting with emptyOn α (which simp can prove is a matroid) and then construct the other examples using duality and restriction.

def Matroid.emptyOn (α : Type u_2) :

The Matroid α with empty ground set.

Equations
  • Matroid.emptyOn α = { E := , Base := fun (x : Set α) => x = , Indep := fun (x : Set α) => x = , indep_iff' := , exists_base := , base_exchange := , maximality := , subset_ground := }
Instances For
    @[simp]
    theorem Matroid.emptyOn_ground {α : Type u_1} :
    @[simp]
    theorem Matroid.emptyOn_base_iff {α : Type u_1} {B : Set α} :
    (Matroid.emptyOn α).Base B B =
    @[simp]
    theorem Matroid.emptyOn_indep_iff {α : Type u_1} {I : Set α} :
    (Matroid.emptyOn α).Indep I I =
    theorem Matroid.ground_eq_empty_iff {α : Type u_1} {M : Matroid α} :
    @[simp]
    theorem Matroid.restrict_empty {α : Type u_1} (M : Matroid α) :
    M.restrict = Matroid.emptyOn α
    theorem Matroid.eq_emptyOn_or_nonempty {α : Type u_1} (M : Matroid α) :
    M = Matroid.emptyOn α M.Nonempty
    theorem Matroid.eq_emptyOn {α : Type u_1} [IsEmpty α] (M : Matroid α) :
    instance Matroid.finite_emptyOn (α : Type u_2) :
    (Matroid.emptyOn α).Finite
    Equations
    • =
    def Matroid.loopyOn {α : Type u_1} (E : Set α) :

    The Matroid α with ground set E whose only base is

    Equations
    Instances For
      @[simp]
      theorem Matroid.loopyOn_ground {α : Type u_1} (E : Set α) :
      @[simp]
      theorem Matroid.loopyOn_indep_iff {α : Type u_1} {E : Set α} {I : Set α} :
      (Matroid.loopyOn E).Indep I I =
      theorem Matroid.eq_loopyOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} :
      M = Matroid.loopyOn E M.E = E XM.E, M.Indep XX =
      @[simp]
      theorem Matroid.loopyOn_base_iff {α : Type u_1} {E : Set α} {B : Set α} :
      (Matroid.loopyOn E).Base B B =
      @[simp]
      theorem Matroid.loopyOn_basis_iff {α : Type u_1} {E : Set α} {I : Set α} {X : Set α} :
      (Matroid.loopyOn E).Basis I X I = X E
      instance Matroid.instFiniteRkLoopyOn {α : Type u_1} {E : Set α} :
      (Matroid.loopyOn E).FiniteRk
      Equations
      • =
      theorem Matroid.Finite.loopyOn_finite {α : Type u_1} {E : Set α} (hE : E.Finite) :
      (Matroid.loopyOn E).Finite
      @[simp]
      theorem Matroid.loopyOn_restrict {α : Type u_1} (E : Set α) (R : Set α) :
      theorem Matroid.empty_base_iff {α : Type u_1} {M : Matroid α} :
      M.Base M = Matroid.loopyOn M.E
      theorem Matroid.eq_loopyOn_or_rkPos {α : Type u_1} (M : Matroid α) :
      M = Matroid.loopyOn M.E M.RkPos
      theorem Matroid.not_rkPos_iff {α : Type u_1} {M : Matroid α} :
      ¬M.RkPos M = Matroid.loopyOn M.E
      def Matroid.freeOn {α : Type u_1} (E : Set α) :

      The Matroid α with ground set E whose only base is E.

      Equations
      Instances For
        @[simp]
        theorem Matroid.freeOn_ground {α : Type u_1} {E : Set α} :
        @[simp]
        @[simp]
        @[simp]
        theorem Matroid.freeOn_base_iff {α : Type u_1} {E : Set α} {B : Set α} :
        (Matroid.freeOn E).Base B B = E
        @[simp]
        theorem Matroid.freeOn_indep_iff {α : Type u_1} {E : Set α} {I : Set α} :
        (Matroid.freeOn E).Indep I I E
        theorem Matroid.freeOn_indep {α : Type u_1} {E : Set α} {I : Set α} (hIE : I E) :
        (Matroid.freeOn E).Indep I
        @[simp]
        theorem Matroid.freeOn_basis_iff {α : Type u_1} {E : Set α} {I : Set α} {X : Set α} :
        (Matroid.freeOn E).Basis I X I = X X E
        @[simp]
        theorem Matroid.freeOn_basis'_iff {α : Type u_1} {E : Set α} {I : Set α} {X : Set α} :
        (Matroid.freeOn E).Basis' I X I = X E
        theorem Matroid.eq_freeOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} :
        M = Matroid.freeOn E M.E = E M.Indep E
        theorem Matroid.ground_indep_iff_eq_freeOn {α : Type u_1} {M : Matroid α} :
        M.Indep M.E M = Matroid.freeOn M.E
        theorem Matroid.freeOn_restrict {α : Type u_1} {E : Set α} {R : Set α} (h : R E) :
        theorem Matroid.restrict_eq_freeOn_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
        M.restrict I = Matroid.freeOn I M.Indep I
        theorem Matroid.Indep.restrict_eq_freeOn {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
        M.restrict I = Matroid.freeOn I
        def Matroid.uniqueBaseOn {α : Type u_1} (I : Set α) (E : Set α) :

        The matroid on E whose unique base is the subset I of E. Intended for use when I ⊆ E; if this not not the case, then the base is I ∩ E.

        Equations
        Instances For
          @[simp]
          theorem Matroid.uniqueBaseOn_ground {α : Type u_1} {E : Set α} {I : Set α} :
          theorem Matroid.uniqueBaseOn_base_iff {α : Type u_1} {E : Set α} {B : Set α} {I : Set α} (hIE : I E) :
          (Matroid.uniqueBaseOn I E).Base B B = I
          @[simp]
          theorem Matroid.uniqueBaseOn_indep_iff' {α : Type u_1} {E : Set α} {I : Set α} {J : Set α} :
          (Matroid.uniqueBaseOn I E).Indep J J I E
          theorem Matroid.uniqueBaseOn_indep_iff {α : Type u_1} {E : Set α} {I : Set α} {J : Set α} (hIE : I E) :
          (Matroid.uniqueBaseOn I E).Indep J J I
          theorem Matroid.uniqueBaseOn_basis_iff {α : Type u_1} {E : Set α} {I : Set α} {X : Set α} {J : Set α} (hX : X E) :
          (Matroid.uniqueBaseOn I E).Basis J X J = X I
          theorem Matroid.uniqueBaseOn_inter_basis {α : Type u_1} {E : Set α} {I : Set α} {X : Set α} (hX : X E) :
          (Matroid.uniqueBaseOn I E).Basis (X I) X
          @[simp]
          theorem Matroid.uniqueBaseOn_dual_eq {α : Type u_1} (I : Set α) (E : Set α) :
          theorem Matroid.uniqueBaseOn_restrict' {α : Type u_1} (I : Set α) (E : Set α) (R : Set α) :
          theorem Matroid.uniqueBaseOn_restrict {α : Type u_1} {E : Set α} {I : Set α} (h : I E) (R : Set α) :