Matroid Deletion

For M : Matroid α and X : Set α, the deletion of X from M is the matroid M ＼ X with ground set M.E \ X, in which a subset of M.E \ X is independent if and only if it is independent in M.

The deletion M ＼ X is equal to the restriction M ↾ (M.E \ X), but is of special importance in the theory because it is the dual notion of contraction, and thus plays a more central and natural role than restriction in many contexts.

Because of the implementation of the restriction M ↾ R allowing R to not be a subset of M.E, the relation M ↾ R ≤r M holds only with the assumption R ⊆ M.E, whereas M ＼ D, being defined as M ↾ (M.E \ D), satisfies M ＼ D ≤r M unconditionally. This is often quite convenient.

Main Declarations

• Matroid.delete M D, written M ＼ D, is the restriction of M to the set M.E \ D, or equivalently the matroid on M.E \ D whose independent sets are the M-independent sets.

Naming conventions

We use the abbreviation deleteElem in lemma names to refer to the deletion M ＼ {e} of a single element e : α from M : Matroid α.

Deletion

def Matroid.delete {α : Type u_1} (M : Matroid α) (D : Set α) : Matroid α

The deletion M ＼ D is the restriction of a matroid M to M.E \ D. Its independent sets are the M-independent subsets of M.E \ D.

Equations

• M.delete D = M.restrict (M.E \ D)

def Matroid.«term_＼_» : Lean.TrailingParserDescr

M ＼ D refers to the deletion of a set D from the matroid M.

Equations

• Matroid.«term_＼_» = Lean.ParserDescr.trailingNode `Matroid.«term_＼_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ＼ ") (Lean.ParserDescr.cat `term 76))

theorem Matroid.delete_eq_restrict {α : Type u_1} (M : Matroid α) (D : Set α) : M.delete D = M.restrict (M.E \ D)

theorem Matroid.restrict_compl {α : Type u_1} (M : Matroid α) (D : Set α) : M.restrict (M.E \ D) = M.delete D

@[simp]

theorem Matroid.delete_compl {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E := by aesop_mat) : M.delete (M.E \ R) = M.restrict R

@[simp]

theorem Matroid.delete_isRestriction {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).IsRestriction M

theorem Matroid.IsRestriction.exists_eq_delete {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) : ∃ D ⊆ M.E, N = M.delete D

theorem Matroid.isRestriction_iff_exists_eq_delete {α : Type u_1} {M N : Matroid α} : N.IsRestriction M ↔ ∃ D ⊆ M.E, N = M.delete D

@[simp]

theorem Matroid.delete_ground {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).E = M.E \ D

theorem Matroid.delete_subset_ground {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).E ⊆ M.E

@[simp]

theorem Matroid.delete_eq_self_iff {α : Type u_1} {M : Matroid α} {D : Set α} : M.delete D = M ↔ Disjoint D M.E

theorem Matroid.delete_eq_self {α : Type u_1} {M : Matroid α} {D : Set α} : Disjoint D M.E → M.delete D = M

Alias of the reverse direction of Matroid.delete_eq_self_iff.

theorem Matroid.deleteElem_eq_self {α : Type u_1} {M : Matroid α} {e : α} (he : e ∉ M.E) : M.delete {e} = M

@[simp]

theorem Matroid.delete_delete {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = M.delete (D₁ ∪ D₂)

theorem Matroid.delete_comm {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = (M.delete D₂).delete D₁

theorem Matroid.delete_inter_ground_eq {α : Type u_1} (M : Matroid α) (D : Set α) : M.delete (D ∩ M.E) = M.delete D

theorem Matroid.delete_eq_delete_iff {α : Type u_1} {M : Matroid α} {D₁ D₂ : Set α} : M.delete D₁ = M.delete D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E

@[simp]

theorem Matroid.delete_empty {α : Type u_1} (M : Matroid α) : M.delete ∅ = M

theorem Matroid.delete_delete_eq_delete_diff {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = (M.delete D₁).delete (D₂ \ D₁)

theorem Matroid.IsRestriction.restrict_delete_of_disjoint {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.IsRestriction M) (hX : Disjoint X N.E) : N.IsRestriction (M.delete X)

theorem Matroid.IsRestriction.isRestriction_deleteElem {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsRestriction M) (he : e ∉ N.E) : N.IsRestriction (M.delete {e})

Independence and Bases

@[simp]

theorem Matroid.delete_indep_iff {α : Type u_1} {M : Matroid α} {I D : Set α} : (M.delete D).Indep I ↔ M.Indep I ∧ Disjoint I D

theorem Matroid.deleteElem_indep_iff {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} : (M.delete {e}).Indep I ↔ M.Indep I ∧ e ∉ I

theorem Matroid.Indep.of_delete {α : Type u_1} {M : Matroid α} {I D : Set α} (h : (M.delete D).Indep I) : M.Indep I

theorem Matroid.Indep.indep_delete_of_disjoint {α : Type u_1} {M : Matroid α} {I D : Set α} (h : M.Indep I) (hID : Disjoint I D) : (M.delete D).Indep I

theorem Matroid.indep_iff_delete_of_disjoint {α : Type u_1} {M : Matroid α} {I D : Set α} (hID : Disjoint I D) : M.Indep I ↔ (M.delete D).Indep I

@[simp]

theorem Matroid.delete_dep_iff {α : Type u_1} {M : Matroid α} {D X : Set α} : (M.delete D).Dep X ↔ M.Dep X ∧ Disjoint X D

@[simp]

theorem Matroid.delete_isBase_iff {α : Type u_1} {M : Matroid α} {B D : Set α} : (M.delete D).IsBase B ↔ M.IsBasis B (M.E \ D)

@[simp]

theorem Matroid.delete_isBasis_iff {α : Type u_1} {M : Matroid α} {I D X : Set α} : (M.delete D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D

@[simp]

theorem Matroid.delete_isBasis'_iff {α : Type u_1} {M : Matroid α} {I D X : Set α} : (M.delete D).IsBasis' I X ↔ M.IsBasis' I (X \ D)

theorem Matroid.IsBasis.of_delete {α : Type u_1} {M : Matroid α} {I D X : Set α} (h : (M.delete D).IsBasis I X) : M.IsBasis I X

theorem Matroid.IsBasis.delete {α : Type u_1} {M : Matroid α} {I D X : Set α} (h : M.IsBasis I X) (hX : Disjoint X D) : (M.delete D).IsBasis I X

theorem Matroid.Coindep.delete_isBase_iff {α : Type u_1} {M : Matroid α} {B D : Set α} (hD : M.Coindep D) : (M.delete D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

theorem Matroid.Coindep.delete_rankPos {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankPos] (hD : M.Coindep D) : (M.delete D).RankPos

theorem Matroid.Coindep.delete_spanning_iff {α : Type u_1} {M : Matroid α} {D S : Set α} (hD : M.Coindep D) : (M.delete D).Spanning S ↔ M.Spanning S ∧ Disjoint S D

Loops, circuits and closure

@[simp]

theorem Matroid.delete_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} : (M.delete D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

@[simp]

theorem Matroid.delete_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} : (M.delete D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

theorem Matroid.IsNonloop.of_delete {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} (h : (M.delete D).IsNonloop e) : M.IsNonloop e

theorem Matroid.isNonloop_iff_delete_of_not_mem {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} (he : e ∉ D) : M.IsNonloop e ↔ (M.delete D).IsNonloop e

theorem Matroid.delete_loops_eq_removeLoops {α : Type u_1} (M : Matroid α) : M.delete M.loops = M.removeLoops

@[simp]

theorem Matroid.delete_isCircuit_iff {α : Type u_1} {M : Matroid α} {D C : Set α} : (M.delete D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

theorem Matroid.IsCircuit.of_delete {α : Type u_1} {M : Matroid α} {D C : Set α} (h : (M.delete D).IsCircuit C) : M.IsCircuit C

theorem Matroid.circuit_iff_delete_of_disjoint {α : Type u_1} {M : Matroid α} {D C : Set α} (hCD : Disjoint C D) : M.IsCircuit C ↔ (M.delete D).IsCircuit C

@[simp]

theorem Matroid.delete_closure_eq {α : Type u_1} (M : Matroid α) (D X : Set α) : (M.delete D).closure X = M.closure (X \ D) \ D

theorem Matroid.delete_closure_eq_of_disjoint {α : Type u_1} (M : Matroid α) {D X : Set α} (hXD : Disjoint X D) : (M.delete D).closure X = M.closure X \ D

@[simp]

theorem Matroid.delete_loops_eq {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).loops = M.loops \ D

theorem Matroid.delete_isColoop_iff {α : Type u_1} {e : α} (M : Matroid α) (D : Set α) : (M.delete D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D

Finiteness

instance Matroid.delete_finitary {α : Type u_1} (M : Matroid α) [M.Finitary] (D : Set α) : (M.delete D).Finitary

instance Matroid.delete_finite {α : Type u_1} {M : Matroid α} {D : Set α} [M.Finite] : (M.delete D).Finite

instance Matroid.delete_rankFinite {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankFinite] : (M.delete D).RankFinite