def Matroid.IsPaving {α : Type u_1} (M : Matroid α) : Prop

A Paving matroid is one whose truncation is uniform, or equivalently one where every dependent set is a single insertion away from being spanning.

Equations

• M.IsPaving = M.truncate.IsUniform

theorem Matroid.IsPaving.truncate_isUniform {α : Type u_1} {M : Matroid α} (hM : M.IsPaving) : M.truncate.IsUniform

theorem Matroid.IsUniform.isPaving {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) : M.IsPaving

@[simp]

theorem Matroid.unifOn_isPaving {α : Type u_1} {E : Set α} {a : ℕ} : (unifOn E a).IsPaving

@[simp]

theorem Matroid.loopyOn_isPaving {α : Type u_1} {E : Set α} : (loopyOn E).IsPaving

@[simp]

theorem Matroid.freeOn_isPaving {α : Type u_1} {E : Set α} : (freeOn E).IsPaving

theorem Matroid.IsPaving.contract {α : Type u_1} {M : Matroid α} (hM : M.IsPaving) (C : Set α) : (M.contract C).IsPaving

theorem Matroid.IsPaving.eRank_contract_le_one_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) : (M.contract D).eRank ≤ 1

theorem Matroid.IsPaving.isCircuit_of_isBase_of_finDiff_of_not_isBase {α : Type u_1} {M : Matroid α} {B C : Set α} (hM : M.IsPaving) (hB : M.IsBase B) (hBC : B.FinDiff C) (hC : ¬M.IsBase C) (hCE : C ⊆ M.E := by aesop_mat) : M.IsCircuit C

In a paving matroid, any nonbase with finite exchange distance from a base is a circuit.

theorem Matroid.IsPaving.isCircuit_insert_diff_singleton_of_isBase_of_not_isBase {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hM : M.IsPaving) (hB : M.IsBase B) (heB : e ∈ M.E \ B) (hfB : f ∈ B) (hB' : ¬M.IsBase (insert e (B \ {f}))) : M.IsCircuit (insert e (B \ {f}))

theorem Matroid.isPaving_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} : M.IsPaving ↔ ∀ (C : Set α), M.IsCircuit C → (M.contract C).eRank ≤ 1

theorem Matroid.IsPaving.exists_insert_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) : ∃ e ∈ M.E, M.Spanning (insert e D)

theorem Matroid.IsPaving.exists_isExchange_isBase_subset_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) : ∃ (B : Set α), M.IsBase B ∧ (B ⊆ D ∨ ∃ (X : Set α), B.IsExchange X ∧ X ⊆ D)

Every dependent set in a paving matroid contains a set that is either a base, or an exchange away from being a base.

theorem Matroid.IsPaving.exists_finDiff_isBase_subset_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) : ∃ (B : Set α) (X : Set α), M.IsBase B ∧ B.FinDiff X ∧ X ⊆ D

theorem Matroid.paving_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} : M.IsPaving ↔ ∀ (C : Set α), M.IsCircuit C → ∃ (e : α), M.Spanning (insert e C)

theorem Matroid.IsPaving.exists_insert_of_dep_of_ssubset {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) (hDE : D ⊂ M.E) : ∃ e ∈ M.E \ D, M.Spanning (insert e D)

theorem Matroid.IsPaving.insert_spanning_of_dep_of_notMem_closure {α : Type u_1} {M : Matroid α} {D : Set α} {e : α} (hM : M.IsPaving) (hD : M.Dep D) (he : e ∈ M.E \ M.closure D) : M.Spanning (insert e D)

theorem Matroid.IsPaving.closure_isHyperplane_of_dep_of_nonspanning {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (hD : M.Dep D) (hDs : M.Nonspanning D) : M.IsHyperplane (M.closure D)

theorem Matroid.IsPaving.restrict_uniform_of_nonspanning {α : Type u_1} {M : Matroid α} {R : Set α} (hM : M.IsPaving) (hRs : M.Nonspanning R) : (M.restrict R).IsUniform

theorem Matroid.IsPaving.eRelRk_ground_le_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (h : M.Dep D) : M.eRelRk D M.E ≤ 1

theorem Matroid.IsPaving.eRank_le_eRk_add_one_of_dep {α : Type u_1} {M : Matroid α} {D : Set α} (hM : M.IsPaving) (h : M.Dep D) : M.eRank ≤ M.eRk D + 1

theorem Matroid.IsPaving.delete {α : Type u_1} {M : Matroid α} (hM : M.IsPaving) (D : Set α) : (M.delete D).IsPaving

theorem Matroid.IsPaving.isMinor {α : Type u_1} {N M : Matroid α} (hM : M.IsPaving) (hNM : N ≤m M) : N.IsPaving

theorem Matroid.IsPaving.exists_diff_indep_of_nonspanning {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M✶.IsPaving) (hXs : M.Nonspanning X) (hne : X.Nonempty) : ∃ f ∈ X, M.Indep (X \ {f})

theorem Matroid.IsPaving.encard_eq_or_eq_of_isCircuit {α : Type u_1} {M : Matroid α} {C : Set α} (hM : M.IsPaving) (hC : M.IsCircuit C) : C.encard = M.eRank ∨ C.encard = M.eRank + 1

theorem Matroid.IsPaving.exists_isCircuit_of_isBase {α : Type u_1} {M : Matroid α} {B : Set α} [M✶.RankPos] (hM : M.IsPaving) (hB : M.IsBase B) : ∃ (C : Set α), M.IsCircuit C ∧ (C \ B).Subsingleton ∧ (B \ C).Subsingleton

Every base in a non-free paving matroid is nearly a circuit.

theorem Matroid.IsPaving.exists_isCircuit_of_spanning {α : Type u_1} {M : Matroid α} {X : Set α} [M✶.RankPos] (hM : M.IsPaving) (hX : M.Spanning X) : ∃ (C : Set α), M.IsCircuit C ∧ (C \ X).Subsingleton

Every spanning set in a non-free paving matroid nearly contains a circuit.

theorem Matroid.IsPaving.exists_isCircuit_of_indep {α : Type u_1} {M : Matroid α} {I : Set α} [M✶.RankPos] (hM : M.IsPaving) (hI : M.Indep I) : ∃ (C : Set α), M.IsCircuit C ∧ (I \ C).Subsingleton

Every independent set in a non-free paving matroid is nearly contained in a circuit.

theorem Matroid.isPaving_iff_girth_ge {α : Type u_1} {M : Matroid α} [M.Finitary] : M.IsPaving ↔ M.eRank ≤ M.girth

structure Matroid.IsSparsePaving {α : Type u_1} (M : Matroid α) : Prop

A SparsePaving matroid is a paving matroid with paving dual, or equivalently one where every nonspanning dependent set is a circuit-hyperplane.

• isPaving : M.IsPaving
• isPaving_dual : M✶.IsPaving

theorem Matroid.isSparsePaving_iff {α : Type u_1} (M : Matroid α) : M.IsSparsePaving ↔ M.IsPaving ∧ M✶.IsPaving

theorem Matroid.IsSparsePaving.dual {α : Type u_1} {M : Matroid α} (h : M.IsSparsePaving) : M✶.IsSparsePaving

theorem Matroid.IsUniform.isSparsePaving {α : Type u_1} {M : Matroid α} (h : M.IsUniform) : M.IsSparsePaving

@[simp]

theorem Matroid.IsSparsePaving_loopyOn {α : Type u_1} (E : Set α) : (loopyOn E).IsSparsePaving

@[simp]

theorem Matroid.IsSparsePaving_freeOn {α : Type u_1} (E : Set α) : (freeOn E).IsSparsePaving

@[simp]

theorem Matroid.IsSparsePaving_unifOn {α : Type u_1} (E : Set α) (a : ℕ) : (unifOn E a).IsSparsePaving

@[simp]

theorem Matroid.dual_isSparsePaving_iff {α : Type u_1} {M : Matroid α} : M✶.IsSparsePaving ↔ M.IsSparsePaving

theorem Matroid.IsSparsePaving.minor {α : Type u_1} {N M : Matroid α} (h : M.IsSparsePaving) (hNM : N ≤m M) : N.IsSparsePaving

theorem Matroid.IsSparsePaving.isCircuitHyperplane_of_dep_of_nonspanning {α : Type u_1} {M : Matroid α} {C : Set α} (hM : M.IsSparsePaving) (hC : M.Dep C) (hCs : M.Nonspanning C) : M.IsCircuitHyperplane C

Every nonspanning dependent set in a sparse paving matroid is a circuit-hyperplane.

theorem Matroid.IsSparsePaving.indep_or_spanning_or_isCircuitHyperplane {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.IsSparsePaving) (hXE : X ⊆ M.E) : M.Indep X ∨ M.Spanning X ∨ M.IsCircuitHyperplane X

theorem Matroid.isSparsePaving_iff_forall_indep_or_spanning_or_isCircuitHyperplane {α : Type u_1} {M : Matroid α} : M.IsSparsePaving ↔ ∀ X ⊆ M.E, M.Indep X ∨ M.Spanning X ∨ M.IsCircuitHyperplane X

theorem Matroid.IsSparsePaving.isBase_or_isCircuitHyperplane_of_finDiff {α : Type u_1} {M : Matroid α} {B X : Set α} (h : M.IsSparsePaving) (hB : M.IsBase B) (hX : X ⊆ M.E) (hBX : B.FinDiff X) : M.IsBase X ∨ M.IsCircuitHyperplane X

theorem Matroid.IsSparsePaving.relax_all_isUniform {α : Type u_1} {M : Matroid α} (h : M.IsSparsePaving) : (M.relax {C : Set α | M.IsCircuitHyperplane C} ⋯).IsUniform

theorem Matroid.IsSparsePaving.exists_eq_relax_unifOn {α : Type u_1} {M : Matroid α} [M.RankFinite] (hM : M.IsSparsePaving) : ∃ (E : Set α) (r : ℕ), M.eRank = ↑r ∧ E = M.E ∧ ∃ (T : Set (Set α)) (h : (unifOn E r).IsLawfulTightening T), M = (unifOn E r).tighten T h

def Matroid.finiteRankSparsePavingOn {α : Type u_1} (E : Set α) (H : Set (Set α)) (r : ℕ) (card_eq : ∀ C ∈ H, C.encard = ↑r) (exchange : H.Pairwise fun (C C' : Set α) => ¬C.IsExchange C') (nonempty : ∀ C ∈ H, C.Nonempty) (ssubset_ground : ∀ C ∈ H, C ⊂ E) : Matroid α

A rank-r sparse paving matroid, specified by its set of circuit-hyperplanes. H should be any set of r-sets, no two differing by a single exchange.

Equations

• Matroid.finiteRankSparsePavingOn E H r card_eq exchange nonempty ssubset_ground = (Matroid.unifOn E r).tighten H ⋯

theorem Matroid.IsSparsePaving.exists_eq_finiteRankSparsePavingOn {α : Type u_1} {M : Matroid α} [M.RankFinite] (hM : M.IsSparsePaving) : ∃ (E : Set α) (r : ℕ) (T : Set (Set α)) (card_eq : ∀ C ∈ T, C.encard = ↑r) (exchange : T.Pairwise fun (C C' : Set α) => ¬C.IsExchange C') (nonempty : ∀ C ∈ T, C.Nonempty) (ssubset_ground : ∀ C ∈ T, C ⊂ E), M.eRank = ↑r ∧ E = M.E ∧ M = finiteRankSparsePavingOn E T r card_eq exchange nonempty ssubset_ground