theorem Matroid.IsBase.exists_exchange_of_isCircuitHyperplane {α : Type u_1} {M : Matroid α} {H B : Set α} {e : α} (hB : M.IsBase B) (hH : M.IsCircuitHyperplane H) (he : e ∈ B) : ∃ f ∈ H \ B, M.IsBase (insert f (B \ {e})) ∨ insert f (B \ {e}) = H

def Matroid.IsLawfulRelaxation {α : Type u_1} (M : Matroid α) (T : Set (Set α)) : Prop

M.IsLawfulRelaxation T means that T is a set of circuit-hyperplanes of M.

Equations

• M.IsLawfulRelaxation T = ∀ ⦃X : Set α⦄, X ∈ T → M.IsCircuitHyperplane X

instance Matroid.GroundedPred.IsLawfulRelaxation : GroundedPred fun {α : Type u_2} => Matroid.IsLawfulRelaxation

instance Matroid.InvariantFun.IsLawfulRelaxation : InvariantFun (fun {α : Type u_2} => Matroid.IsLawfulRelaxation) fun {β : Type u_3} => Matroid.IsLawfulRelaxation

theorem Matroid.IsLawfulRelaxation.map {α : Type u_1} {M : Matroid α} {T : Set (Set α)} {β : Type u_2} {f : α → β} (h : M.IsLawfulRelaxation T) (hf : Set.InjOn f M.E) : (M.map f hf).IsLawfulRelaxation (Set.image f '' T)

theorem Matroid.IsLawfulRelaxation.ssubset_ground {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (hX : X ∈ T) : X ⊂ M.E

theorem Matroid.IsLawfulRelaxation.nonempty {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (hX : X ∈ T) : X.Nonempty

theorem Matroid.IsLawfulRelaxation.antichain {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (T ∪ {B : Set α | M.IsBase B})

theorem Matroid.IsLawfulRelaxation.single {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuitHyperplane C) : M.IsLawfulRelaxation {C}

theorem Matroid.IsLawfulRelaxation.all {α : Type u_1} (M : Matroid α) : M.IsLawfulRelaxation {C : Set α | M.IsCircuitHyperplane C}

the set of all circuit hyperplanes is a lawful relaxation.

def Matroid.relax {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulRelaxation T) : Matroid α

Relax a collection T of circuit-hyperplanes of a matroid M to obtain a new matroid whose bases are the old bases together with the sets in T.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.relax_E {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulRelaxation T) : (M.relax T hT).E = M.E

@[simp]

theorem Matroid.relax_Indep {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulRelaxation T) (I : Set α) : (M.relax T hT).Indep I = (M.Indep I ∨ I ∈ T)

@[simp]

theorem Matroid.relax_IsBase {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulRelaxation T) (B : Set α) : (M.relax T hT).IsBase B = (M.IsBase B ∨ B ∈ T)

theorem Matroid.IsLawfulRelaxation.dual {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) : M✶.IsLawfulRelaxation ((fun (X : Set α) => M.E \ X) '' T)

@[simp]

theorem Matroid.relax_dual {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) : (M.relax T h)✶ = M✶.relax ((fun (X : Set α) => M.E \ X) '' T) ⋯

@[simp]

theorem Matroid.relax_spanning_iff {α : Type u_1} {M : Matroid α} {T : Set (Set α)} {S : Set α} (h : M.IsLawfulRelaxation T) : (M.relax T h).Spanning S ↔ M.Spanning S ∨ S ∈ T

@[simp]

theorem Matroid.relax_dep_iff {α : Type u_1} {M : Matroid α} {T : Set (Set α)} {D : Set α} (h : M.IsLawfulRelaxation T) : (M.relax T h).Dep D ↔ M.Dep D ∧ D ∉ T

@[simp]

theorem Matroid.relax_eRank_eq {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) : (M.relax T h).eRank = M.eRank

@[simp]

theorem Matroid.relax_empty {α : Type u_1} (M : Matroid α) : M.relax ∅ ⋯ = M

theorem Matroid.relax_map {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) : (M.relax T h).map f ⋯ = (M.map f hf).relax (Set.image f '' T) ⋯

theorem Matroid.relax_nonspanning_iff {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) : (M.relax T h).Nonspanning X ↔ M.Nonspanning X ∧ X ∉ T

theorem Matroid.relax_isCircuit_iff {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {C : Set α} : (M.relax T h).IsCircuit C ↔ M.IsCircuit C ∧ C ∉ T ∨ C ⊆ M.E ∧ ∃ e ∈ C, C \ {e} ∈ T

theorem Matroid.relax_isNonspanningCircuit_iff {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {C : Set α} : (M.relax T h).IsNonspanningCircuit C ↔ M.IsNonspanningCircuit C ∧ C ∉ T

instance Matroid.rankPos_relax {α : Type u_1} {M : Matroid α} {T : Set (Set α)} [M.RankPos] (h : M.IsLawfulRelaxation T) : (M.relax T h).RankPos

instance Matroid.rankFinite_relax {α : Type u_1} {M : Matroid α} {T : Set (Set α)} [M.RankFinite] (h : M.IsLawfulRelaxation T) : (M.relax T h).RankFinite

instance Matroid.finite_relax {α : Type u_1} {M : Matroid α} {T : Set (Set α)} [M.Finite] (h : M.IsLawfulRelaxation T) : (M.relax T h).Finite

def Matroid.IsCircuitHyperplane.relax {α : Type u_1} {M : Matroid α} {C : Set α} (h : M.IsCircuitHyperplane C) : Matroid α

Change a single circuit-hyperplane C of M to a base.

Equations

• h.relax = M.relax {C} ⋯

@[simp]

theorem Matroid.IsCircuitHyperplane.relax_ground {α : Type u_1} {M : Matroid α} {C : Set α} (h : M.IsCircuitHyperplane C) : h.relax.E = M.E

@[simp]

theorem Matroid.IsCircuitHyperplane.relax_isBase_iff {α : Type u_1} {M : Matroid α} {B C : Set α} (h : M.IsCircuitHyperplane C) : h.relax.IsBase B ↔ M.IsBase B ∨ B = C

@[simp]

theorem Matroid.IsCircuitHyperplane.relax_indep_iff {α : Type u_1} {M : Matroid α} {I C : Set α} (h : M.IsCircuitHyperplane C) : h.relax.Indep I ↔ M.Indep I ∨ I = C

theorem Matroid.IsLawfulRelaxation.contract {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (C : Set α) : (M.contract C).IsLawfulRelaxation ((fun (x : Set α) => x \ C) '' {H : Set α | H ∈ T ∧ C ⊂ H})

theorem Matroid.IsLawfulRelaxation.delete {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (D : Set α) : (M.delete D).IsLawfulRelaxation {H : Set α | H ∈ T ∧ D ⊂ M.E \ H}

theorem Matroid.IsLawfulRelaxation.contract_delete {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (C D : Set α) : ((M.contract C).delete D).IsLawfulRelaxation ((fun (X : Set α) => X \ C) '' {H : Set α | H ∈ T ∧ C ⊂ H ∧ D ⊂ M.E \ H})

theorem Matroid.relax_delete {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {D : Set α} (hD : D ⊆ M.E := by aesop_mat) (hDT : M.E \ D ∉ T) : (M.relax T h).delete D = (M.delete D).relax {H : Set α | H ∈ T ∧ D ⊂ M.E \ H} ⋯

Relaxation commutes with deletion; if T is a set of circuit-hyperplanes of M, and T₀ is the subset of T that survive as circuit-hyperplanes in a deletion M ＼ D, then the relaxation of T₀ in M ＼ D is obtained from that of T in M by deleting D.

Unfortunately, there is one technical exception; if C ∈ T, and D = M.E \ C, then C is a circuit but not circuit-hyperplane of M ＼ D, so there are no relaxations at all in M ＼ D. However, relaxing C first then deleting D gives a free matroid.

theorem Matroid.relax_contract {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {C : Set α} (hC : C ∉ T) (hCE : C ⊆ M.E := by aesop_mat) : (M.relax T h).contract C = (M.contract C).relax ((fun (x : Set α) => x \ C) '' {H : Set α | H ∈ T ∧ C ⊂ H}) ⋯

theorem Matroid.relax_delete_of_coindep {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {D : Set α} (hD : M.Coindep D) : (M.relax T h).delete D = (M.delete D).relax {H : Set α | H ∈ T ∧ D ⊂ M.E \ H} ⋯

theorem Matroid.relax_contract_of_indep {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) {C : Set α} (hC : M.Indep C) : (M.relax T h).contract C = (M.contract C).relax ((fun (x : Set α) => x \ C) '' {H : Set α | H ∈ T ∧ C ⊂ H}) ⋯

structure Matroid.IsLawfulTightening {α : Type u_1} (M : Matroid α) (T : Set (Set α)) : Prop

A collection of free bases, with no pair of symmetric difference two. Removing these sets from the collection of bases gives a matroid. Doing this with some bases of a uniform matroid gives a sparse paving matroid.

• isFreeBase_of_mem ⦃B : Set α⦄ : B ∈ T → M.IsFreeBase B
• pairwise_not_isExchange : T.Pairwise fun (B B' : Set α) => ¬B.IsExchange B'
• ground_notMem : M.E ∉ T
• empty_notMem : ∅ ∉ T

theorem Matroid.IsLawfulTightening.ssubset_ground {α : Type u_1} {M : Matroid α} {B : Set α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) (hBT : B ∈ T) : B ⊂ M.E

theorem Matroid.IsLawfulTightening.nonempty {α : Type u_1} {M : Matroid α} {B : Set α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) (hBT : B ∈ T) : B.Nonempty

theorem Matroid.IsLawfulTightening.notMem_of_exchange {α : Type u_1} {M : Matroid α} {B : Set α} {T : Set (Set α)} {B' : Set α} (hT : M.IsLawfulTightening T) (hBT : B ∈ T) (hB' : B'.IsExchange B) : B' ∉ T

theorem Matroid.IsLawfulTightening.exists_notMem_between {α : Type u_1} {M : Matroid α} {I : Set α} {T : Set (Set α)} {S : Set α} (hT : M.IsLawfulTightening T) (hI : M.Indep I) (hS : M.Spanning S) (hIS : I ⊆ S) (hIT : I ∉ T) (hST : S ∉ T) : ∃ (B : Set α), I ⊆ B ∧ B ⊆ S ∧ M.IsBase B ∧ B ∉ T

theorem Matroid.IsLawfulTightening.dual {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (h : M.IsLawfulTightening T) : M✶.IsLawfulTightening ((fun (B : Set α) => M.E \ B) '' T)

def Matroid.tighten {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulTightening T) : Matroid α

Given a collection of free bases of a matroid M, with no pair having symmetric difference of size two, we can declare all these to be nonbases, and still have a matroid.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.tighten_Indep {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulTightening T) (I : Set α) : (M.tighten T hT).Indep I = (M.Indep I ∧ I ∉ T)

@[simp]

theorem Matroid.tighten_E {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulTightening T) : (M.tighten T hT).E = M.E

@[simp]

theorem Matroid.tighten_IsBase {α : Type u_1} (M : Matroid α) (T : Set (Set α)) (hT : M.IsLawfulTightening T) (B : Set α) : (M.tighten T hT).IsBase B = (M.IsBase B ∧ B ∉ T)

@[simp]

theorem Matroid.IsLawfulTightening.matroid_dual {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) : (M.tighten T hT)✶ = M✶.tighten ((fun (B : Set α) => M.E \ B) '' T) ⋯

theorem Matroid.IsLawfulTightening.isCircuitHyperplane_tighten {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) (hX : X ∈ T) : (M.tighten T hT).IsCircuitHyperplane X

theorem Matroid.IsLawfulTightening.encard_eq_eRank_of_mem {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (h : M.IsLawfulTightening T) (hX : X ∈ T) : X.encard = M.eRank

@[simp]

theorem Matroid.IsLawfulTightening_empty {α : Type u_1} (M : Matroid α) : M.IsLawfulTightening ∅

@[simp]

theorem Matroid.tighten_empty {α : Type u_1} (M : Matroid α) : M.tighten ∅ ⋯ = M

def Matroid.tightenSingle {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsFreeBase B) (hBne : B.Nonempty) (hBE : B ≠ M.E) : Matroid α

Tighten a single free base.

Equations

• Matroid.tightenSingle hB hBne hBE = M.tighten {B} ⋯

@[simp]

theorem Matroid.tightenSingle_E {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsFreeBase B) (hBne : B.Nonempty) (hBE : B ≠ M.E) : (tightenSingle hB hBne hBE).E = M.E

@[simp]

theorem Matroid.tightenSingle_Indep {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsFreeBase B) (hBne : B.Nonempty) (hBE : B ≠ M.E) (I : Set α) : (tightenSingle hB hBne hBE).Indep I = (M.Indep I ∧ ¬I = B)

@[simp]

theorem Matroid.tightenSingle_IsBase {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsFreeBase B) (hBne : B.Nonempty) (hBE : B ≠ M.E) (B✝ : Set α) : (tightenSingle hB hBne hBE).IsBase B✝ = (M.IsBase B✝ ∧ ¬B✝ = B)

theorem Matroid.IsLawfulRelaxation.isFreeBase_relax {α : Type u_1} {M : Matroid α} {X : Set α} {T : Set (Set α)} (h : M.IsLawfulRelaxation T) (hX : X ∈ T) : (M.relax T h).IsFreeBase X

theorem Matroid.IsLawfulRelaxation.isLawfulTightening_relax {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (hT : M.IsLawfulRelaxation T) : (M.relax T hT).IsLawfulTightening T

@[simp]

theorem Matroid.IsLawfulRelaxation.tighten_relax {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (hT : M.IsLawfulRelaxation T) : (M.relax T hT).tighten T ⋯ = M

theorem Matroid.IsLawfulTightening.isLawfulRelaxation_tighten {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) : (M.tighten T hT).IsLawfulRelaxation T

@[simp]

theorem Matroid.IsLawfulTightening.relax_tighten {α : Type u_1} {M : Matroid α} {T : Set (Set α)} (hT : M.IsLawfulTightening T) : (M.tighten T hT).relax T ⋯ = M