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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Matroid.emptyOn_ground {α : Type u_1} :
(emptyOn α).E =
@[simp]
theorem Matroid.emptyOn_isBase_iff {α : Type u_1} {B : Set α} :
@[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 . The elements are all 'loops' - see Matroid.IsLoop and Matroid.loopyOn_isLoop_iff.

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_isBase_iff {α : Type u_1} {E B : Set α} :
@[simp]
theorem Matroid.loopyOn_isBasis_iff {α : Type u_1} {E I X : Set α} :
(loopyOn E).IsBasis I X I = X E
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_isBase_iff {α : Type u_1} {M : Matroid α} :
theorem Matroid.not_rankPos_iff {α : Type u_1} {M : Matroid α} :
instance Matroid.loopyOn_rankFinite {α : 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_isBase_iff {α : Type u_1} {E B : Set α} :
(freeOn E).IsBase 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_isBasis_iff {α : Type u_1} {E I X : Set α} :
(freeOn E).IsBasis I X I = X X E
@[simp]
theorem Matroid.freeOn_isBasis'_iff {α : Type u_1} {E I X : Set α} :
(freeOn E).IsBasis' 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_rankPos {α : 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_isBase_iff {α : Type u_1} {E B I : Set α} (hIE : I E) :
(uniqueBaseOn I E).IsBase 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_isBasis_iff {α : Type u_1} {E I X J : Set α} (hX : X E) :
(uniqueBaseOn I E).IsBasis J X J = X I
theorem Matroid.uniqueBaseOn_inter_isBasis {α : Type u_1} {E I X : Set α} (hX : X E) :
(uniqueBaseOn I E).IsBasis (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_rankFinite {α : Type u_1} {E I : Set α} (hI : I.Finite) :
instance Matroid.uniqueBaseOn_finitary {α : Type u_1} {E I : Set α} :
theorem Matroid.uniqueBaseOn_rankPos {α : Type u_1} {E I : Set α} (hIE : I E) (hI : I.Nonempty) :