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 := }
@[simp]
theorem Matroid.emptyOn_ground {α : Type u_1} :
(emptyOn α).E =
@[simp]
theorem Matroid.emptyOn_base_iff {α : Type u_1} {B : Set α} :
(emptyOn α).Base B B =
@[simp]
theorem Matroid.emptyOn_indep_iff {α : Type u_1} {I : Set α} :
(emptyOn α).Indep I I =
theorem Matroid.ground_eq_empty_iff {α : Type u_1} {M : Matroid α} :
M.E = M = emptyOn α
@[simp]
theorem Matroid.emptyOn_dual_eq {α : Type u_1} :
@[simp]
theorem Matroid.restrict_empty {α : Type u_1} (M : Matroid α) :
theorem Matroid.eq_emptyOn {α : Type u_1} [IsEmpty α] (M : Matroid α) :
M = emptyOn α
def Matroid.loopyOn {α : Type u_1} (E : Set α) :

The Matroid α with ground set E whose only base is

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

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

Equations
@[simp]
theorem Matroid.freeOn_ground {α : Type u_1} {E : Set α} :
(freeOn E).E = E
@[simp]
theorem Matroid.freeOn_dual_eq {α : Type u_1} {E : Set α} :
@[simp]
theorem Matroid.loopyOn_dual_eq {α : Type u_1} {E : Set α} :
@[simp]
theorem Matroid.freeOn_empty (α : Type u_2) :
@[simp]
theorem Matroid.freeOn_base_iff {α : Type u_1} {E B : Set α} :
(freeOn E).Base B B = E
@[simp]
theorem Matroid.freeOn_indep_iff {α : Type u_1} {E I : Set α} :
(freeOn E).Indep I I E
theorem Matroid.freeOn_indep {α : Type u_1} {E I : Set α} (hIE : I E) :
@[simp]
theorem Matroid.freeOn_basis_iff {α : Type u_1} {E I X : Set α} :
(freeOn E).Basis I X I = X X E
@[simp]
theorem Matroid.freeOn_basis'_iff {α : Type u_1} {E I X : Set α} :
(freeOn E).Basis' I X I = X E
theorem Matroid.eq_freeOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} :
M = freeOn E M.E = E M.Indep E
theorem Matroid.freeOn_restrict {α : Type u_1} {E R : Set α} (h : R E) :
theorem Matroid.restrict_eq_freeOn_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
theorem Matroid.Indep.restrict_eq_freeOn {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
instance Matroid.freeOn_finitary {α : Type u_1} {E : Set α} :
theorem Matroid.freeOn_rkPos {α : Type u_1} {E : Set α} (hE : E.Nonempty) :
def Matroid.uniqueBaseOn {α : Type u_1} (I 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
@[simp]
theorem Matroid.uniqueBaseOn_ground {α : Type u_1} {E I : Set α} :
(uniqueBaseOn I E).E = E
theorem Matroid.uniqueBaseOn_base_iff {α : Type u_1} {E B I : Set α} (hIE : I E) :
(uniqueBaseOn I E).Base B B = I
@[simp]
theorem Matroid.uniqueBaseOn_indep_iff' {α : Type u_1} {E I J : Set α} :
(uniqueBaseOn I E).Indep J J I E
theorem Matroid.uniqueBaseOn_indep_iff {α : Type u_1} {E I J : Set α} (hIE : I E) :
theorem Matroid.uniqueBaseOn_basis_iff {α : Type u_1} {E I X J : Set α} (hX : X E) :
(uniqueBaseOn I E).Basis J X J = X I
theorem Matroid.uniqueBaseOn_inter_basis {α : Type u_1} {E I X : Set α} (hX : X E) :
(uniqueBaseOn I E).Basis (X I) X
@[simp]
theorem Matroid.uniqueBaseOn_dual_eq {α : Type u_1} (I E : Set α) :
@[simp]
theorem Matroid.uniqueBaseOn_self {α : Type u_1} (I : Set α) :
@[simp]
theorem Matroid.uniqueBaseOn_empty {α : Type u_1} (I : Set α) :
theorem Matroid.uniqueBaseOn_restrict' {α : Type u_1} (I E R : Set α) :
theorem Matroid.uniqueBaseOn_restrict {α : Type u_1} {E I : Set α} (h : I E) (R : Set α) :
theorem Matroid.uniqueBaseOn_finiteRk {α : Type u_1} {E I : Set α} (hI : I.Finite) :
instance Matroid.uniqueBaseOn_finitary {α : Type u_1} {E I : Set α} :
theorem Matroid.uniqueBaseOn_rkPos {α : Type u_1} {E I : Set α} (hIE : I E) (hI : I.Nonempty) :