Matroid Closure

A Flat of a matroid M is a combinatorial analogue of a subspace of a vector space, and is defined to be a subset F of the ground set of M such that for each basis I for M, every set having I as a basis is contained in F.

The closure of a set X in a matroid M is the intersection of all flats of M containing X. This is a combinatorial analogue of the linear span of a set of vectors.

For M : Matroid α, this file defines a predicate M.Flat : Set α → Prop and a function M.closure : Set α → Set α corresponding to these notions, and develops API for the latter. API for Matroid.Flat will appear in another file; we include the definition here since it is used in the definition of Matroid.closure.

We also define a predicate Spanning, to describe a set whose closure is the entire ground set.

Main definitions

• For M : Matroid α and F : Set α, M.Flat F means that F is a flat of M.
• For M : Matroid α and X : Set α, M.closure X is the closure of X in M.
• For M : Matroid α and X : ↑(Iic M.E) (i.e. a bundled subset of M.E), M.subtypeClosure X is the closure of X, viewed as a term in ↑(Iic M.E). This is a ClosureOperator on ↑(Iic M.E).
• For M : Matroid α and S ⊆ M.E, M.Spanning S means that S has closure equal to M.E, or equivalently that S contains a base of M.

Implementation details

If X : Set α satisfies X ⊆ M.E, then it is clear how M.closure X should be defined. But M.closure X also needs to be defined for all X : Set α, so a convention is needed for how it handles sets containing junk elements outside M.E. All such choices come with tradeoffs. Provided that M.closure X has already been defined for X ⊆ M.E, the two best candidates for extending it to all X seem to be:

(1) The function for which M.closure X = M.closure (X ∩ M.E) for all X : Set α

(2) The function for which M.closure X = M.closure (X ∩ M.E) ∪ X for all X : Set α

For both options, the function closure is monotone and idempotent with no assumptions on X.

Choice (1) has the advantage that M.closure X ⊆ M.E holds for all X without the assumption that X ⊆ M.E, which is very nice for aesop_mat. It is also fairly convenient to rewrite M.closure X to M.closure (X ∩ M.E) when one needs to work with a subset of the ground set. Its disadvantage is that the statement X ⊆ M.closure X is only true provided that X ⊆ M.E.

Choice (2) has the reverse property: we would have X ⊆ M.closure X for all X, but the condition M.closure X ⊆ M.E requires X ⊆ M.E to hold. It has a couple of other advantages too: it is actually the closure function of a matroid on α with ground set univ (specifically, the direct sum of M and a free matroid on M.Eᶜ), and because of this, it is an example of a ClosureOperator on α, which in turn gives access to nice existing API for both ClosureOperator and GaloisInsertion. This also relates to flats; F ⊆ M.E ∧ ClosureOperator.IsClosed F is equivalent to M.Flat F. (All of this fails for choice (1), since X ⊆ M.closure X is required for a ClosureOperator, but isn't true for non-subsets of M.E)

The API that choice (2) would offer is very beguiling, but after extensive experimentation in an external repo, it seems that (1) is far less rough around the edges in practice, so we go with (1). It may be helpful at some point to define a primed version Matroid.closure' : ClosureOperator (Set α) corresponding to choice (2). Failing that, the ClosureOperator/GaloisInsertion API is still available on the subtype ↑(Iic M.E) via Matroid.SubtypeClosure, albeit less elegantly.

Naming conventions

In lemma names, the words spanning and flat are used as suffixes, for instance we have ground_spanning rather than spanning_ground.

structure Matroid.Flat {α : Type u_2} (M : Matroid α) (F : Set α) : Prop

A flat is a maximal set having a given basis

• subset_of_basis_of_basis : ∀ ⦃I X : Set α⦄, M.Basis I F → M.Basis I X → X ⊆ F
• subset_ground : F ⊆ M.E

theorem Matroid.flat_iff {α : Type u_2} (M : Matroid α) (F : Set α) : M.Flat F ↔ (∀ ⦃I X : Set α⦄, M.Basis I F → M.Basis I X → X ⊆ F) ∧ F ⊆ M.E

@[simp]

theorem Matroid.ground_flat {α : Type u_2} (M : Matroid α) : M.Flat M.E

theorem Matroid.Flat.iInter {α : Type u_2} {M : Matroid α} {ι : Type u_3} [Nonempty ι] {Fs : ι → Set α} (hFs : ∀ (i : ι), M.Flat (Fs i)) : M.Flat (⋂ (i : ι), Fs i)

def Matroid.subtypeClosure {α : Type u_2} (M : Matroid α) : ClosureOperator ↑(Set.Iic M.E)

The property of being a flat gives rise to a ClosureOperator on the subsets of M.E, in which the IsClosed sets correspond to Flats. (We can't define such an operator on all of Set α, since this would incorrectly force univ to always be a flat.)

Equations

• M.subtypeClosure = ClosureOperator.ofCompletePred (fun (F : ↑(Set.Iic M.E)) => M.Flat ↑F) ⋯

theorem Matroid.flat_iff_isClosed {α : Type u_2} {M : Matroid α} {F : Set α} : M.Flat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩

theorem Matroid.isClosed_iff_flat {α : Type u_2} {M : Matroid α} {F : ↑(Set.Iic M.E)} : M.subtypeClosure.IsClosed F ↔ M.Flat ↑F

def Matroid.closure {α : Type u_2} (M : Matroid α) (X : Set α) : Set α

The closure of X ⊆ M.E is the intersection of all the flats of M containing X. A set X that doesn't satisfy X ⊆ M.E has the junk value M.closure X := M.closure (X ∩ M.E).

Equations

• M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ∩ M.E ⊆ F}

theorem Matroid.closure_def {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ∩ M.E ⊆ F}

theorem Matroid.closure_def' {α : Type u_2} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ⊆ F}

theorem Matroid.closure_eq_subtypeClosure {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

theorem Matroid.closure_subset_ground {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ⊆ M.E

@[simp]

theorem Matroid.ground_subset_closure_iff {α : Type u_2} {M : Matroid α} {X : Set α} : M.E ⊆ M.closure X ↔ M.closure X = M.E

@[simp]

theorem Matroid.closure_inter_ground {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (X ∩ M.E) = M.closure X

theorem Matroid.inter_ground_subset_closure {α : Type u_2} (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X

theorem Matroid.mem_closure_iff_forall_mem_flat {α : Type u_2} {M : Matroid α} {e : α} (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : e ∈ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → e ∈ F

theorem Matroid.subset_closure_iff_forall_subset_flat {α : Type u_2} {M : Matroid α} {Y : Set α} (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : Y ⊆ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → Y ⊆ F

theorem Matroid.subset_closure {α : Type u_2} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ M.closure X

theorem Matroid.Flat.closure {α : Type u_2} {M : Matroid α} {F : Set α} (hF : M.Flat F) : M.closure F = F

@[simp]

theorem Matroid.closure_ground {α : Type u_2} (M : Matroid α) : M.closure M.E = M.E

@[simp]

theorem Matroid.closure_univ {α : Type u_2} (M : Matroid α) : M.closure Set.univ = M.E

theorem Matroid.closure_subset_closure {α : Type u_2} {X Y : Set α} (M : Matroid α) (h : X ⊆ Y) : M.closure X ⊆ M.closure Y

theorem Matroid.closure_mono {α : Type u_2} (M : Matroid α) : Monotone M.closure

@[simp]

theorem Matroid.closure_closure {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (M.closure X) = M.closure X

theorem Matroid.closure_subset_closure_of_subset_closure {α : Type u_2} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ M.closure Y) : M.closure X ⊆ M.closure Y

theorem Matroid.closure_subset_closure_iff_subset_closure {α : Type u_2} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y

theorem Matroid.subset_closure_of_subset {α : Type u_2} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : X ⊆ M.closure Y

theorem Matroid.subset_closure_of_subset' {α : Type u_2} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ M.closure Y

theorem Matroid.exists_of_closure_ssubset {α : Type u_2} {M : Matroid α} {X Y : Set α} (hXY : M.closure X ⊂ M.closure Y) : ∃ e ∈ Y, e ∉ M.closure X

theorem Matroid.mem_closure_of_mem {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (h : e ∈ X) (hX : X ⊆ M.E := by aesop_mat) : e ∈ M.closure X

theorem Matroid.mem_closure_of_mem' {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (heX : e ∈ X) (h : e ∈ M.E := by aesop_mat) : e ∈ M.closure X

theorem Matroid.not_mem_of_mem_diff_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E \ M.closure X) : e ∉ X

theorem Matroid.mem_ground_of_mem_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : e ∈ M.E

theorem Matroid.closure_iUnion_closure_eq_closure_iUnion {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) : M.closure (⋃ (i : ι), M.closure (Xs i)) = M.closure (⋃ (i : ι), Xs i)

theorem Matroid.closure_iUnion_congr {ι : Type u_1} {α : Type u_2} {M : Matroid α} (Xs Ys : ι → Set α) (h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ (i : ι), Xs i) = M.closure (⋃ (i : ι), Ys i)

theorem Matroid.closure_biUnion_closure_eq_closure_sUnion {α : Type u_2} (M : Matroid α) (Xs : Set (Set α)) : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

theorem Matroid.closure_biUnion_closure_eq_closure_biUnion {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) (A : Set ι) : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

theorem Matroid.closure_biUnion_congr {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs Ys : ι → Set α) (A : Set ι) (h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)

theorem Matroid.closure_closure_union_closure_eq_closure_union {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_union_closure_right_eq {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_union_closure_left_eq {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_insert_closure_eq_closure_insert {α : Type u_2} (M : Matroid α) (e : α) (X : Set α) : M.closure (insert e (M.closure X)) = M.closure (insert e X)

@[simp]

theorem Matroid.closure_union_closure_empty_eq {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ∪ M.closure ∅ = M.closure X

@[simp]

theorem Matroid.closure_empty_union_closure_eq {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure ∅ ∪ M.closure X = M.closure X

theorem Matroid.closure_insert_eq_of_mem_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : M.closure (insert e X) = M.closure X

theorem Matroid.mem_closure_self {α : Type u_2} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) : e ∈ M.closure {e}

theorem Matroid.Indep.closure_eq_setOf_basis_insert {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.closure I = {x : α | M.Basis I (insert x I)}

theorem Matroid.Indep.insert_basis_iff_mem_closure {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Basis I (insert e I) ↔ e ∈ M.closure I

theorem Matroid.Indep.basis_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Basis I (M.closure I)

theorem Matroid.Basis.closure_eq_closure {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis I X) : M.closure I = M.closure X

theorem Matroid.Basis.closure_eq_right {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis I (M.closure X)) : M.closure I = M.closure X

theorem Matroid.Basis'.closure_eq_closure {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis' I X) : M.closure I = M.closure X

theorem Matroid.Basis.subset_closure {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis I X) : X ⊆ M.closure I

theorem Matroid.Basis'.basis_closure_right {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis' I X) : M.Basis I (M.closure X)

theorem Matroid.Basis.basis_closure_right {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.Basis I X) : M.Basis I (M.closure X)

theorem Matroid.Indep.mem_closure_iff {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

theorem Matroid.Indep.mem_closure_iff' {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

theorem Matroid.Indep.insert_dep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Dep (insert e I) ↔ e ∈ M.closure I \ I

theorem Matroid.Indep.mem_closure_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : e ∈ M.closure I ↔ M.Dep (insert e I)

theorem Matroid.Indep.not_mem_closure_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ M.E := by aesop_mat) : e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I

theorem Matroid.Indep.not_mem_closure_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.E := by aesop_mat) : e ∉ M.closure I ↔ M.Indep (insert e I)

theorem Matroid.Indep.insert_indep_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I

theorem Matroid.Indep.insert_indep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

theorem Matroid.insert_indep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

theorem Matroid.Indep.insert_diff_indep_iff {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep (I \ {e})) (heI : e ∈ I) : M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

This can be used for rewriting if the LHS is inside a binder and whether f = e is unknown.

theorem Matroid.Indep.basis_of_subset_of_subset_closure {α : Type u_2} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hXI : X ⊆ M.closure I) : M.Basis I X

theorem Matroid.basis_iff_indep_subset_closure {α : Type u_2} {M : Matroid α} {X I : Set α} : M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I

theorem Matroid.Indep.base_of_ground_subset_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : M.E ⊆ M.closure I) : M.Base I

theorem Matroid.Base.closure_eq {α : Type u_2} {M : Matroid α} {B : Set α} (hB : M.Base B) : M.closure B = M.E

theorem Matroid.Base.closure_of_superset {α : Type u_2} {M : Matroid α} {X B : Set α} (hB : M.Base B) (hBX : B ⊆ X) : M.closure X = M.E

theorem Matroid.base_iff_indep_closure_eq {α : Type u_2} {M : Matroid α} {B : Set α} : M.Base B ↔ M.Indep B ∧ M.closure B = M.E

theorem Matroid.Indep.base_iff_ground_subset_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Base I ↔ M.E ⊆ M.closure I

theorem Matroid.Indep.closure_inter_eq_self_of_subset {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJI : J ⊆ I) : M.closure J ∩ I = J

theorem Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset {α : Type u_2} {M : Matroid α} {I : Set α} {Js : Set (Set α)} (hI : M.Indep I) (hne : Js.Nonempty) (hIs : ∀ J ∈ Js, J ⊆ I) : M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J

For a nonempty collection of subsets of a given independent set, the closure of the intersection is the intersection of the closure.

theorem Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep {α : Type u_2} {M : Matroid α} {ι : Sort u_3} [hι : Nonempty ι] (Is : ι → Set α) (h : M.Indep (⋃ (i : ι), Is i)) : M.closure (⋂ (i : ι), Is i) = ⋂ (i : ι), M.closure (Is i)

theorem Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep {α : Type u_2} {M : Matroid α} (Is : Set (Set α)) (hIs : Is.Nonempty) (h : M.Indep (⋃₀ Is)) : M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I

theorem Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep {α : Type u_2} {M : Matroid α} {ι : Type u_4} {A : Set ι} (hA : A.Nonempty) {I : ι → Set α} (h : M.Indep (⋃ i ∈ A, I i)) : M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

theorem Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset {α : Type u_2} {M : Matroid α} {ι : Sort u_3} {I : Set α} [Nonempty ι] {Js : ι → Set α} (hI : M.Indep I) (hJs : ∀ (i : ι), Js i ⊆ I) : M.closure (⋂ (i : ι), Js i) = ⋂ (i : ι), M.closure (Js i)

theorem Matroid.Indep.closure_inter_eq_inter_closure {α : Type u_2} {M : Matroid α} {I J : Set α} (h : M.Indep (I ∪ J)) : M.closure (I ∩ J) = M.closure I ∩ M.closure J

theorem Matroid.basis_iff_basis_closure_of_subset {α : Type u_2} {M : Matroid α} {X I : Set α} (hIX : I ⊆ X) (hX : X ⊆ M.E := by aesop_mat) : M.Basis I X ↔ M.Basis I (M.closure X)

theorem Matroid.basis_iff_basis_closure_of_subset' {α : Type u_2} {M : Matroid α} {X I : Set α} (hIX : I ⊆ X) : M.Basis I X ↔ M.Basis I (M.closure X) ∧ X ⊆ M.E

theorem Matroid.basis'_iff_basis_closure {α : Type u_2} {M : Matroid α} {X I : Set α} : M.Basis' I X ↔ M.Basis I (M.closure X) ∧ I ⊆ X

theorem Matroid.exists_basis_inter_ground_basis_closure {α : Type u_2} (M : Matroid α) (X : Set α) : ∃ (I : Set α), M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)

theorem Matroid.Basis.basis_of_closure_eq_closure {α : Type u_2} {M : Matroid α} {X Y I : Set α} (hI : M.Basis I X) (hY : I ⊆ Y) (h : M.closure X = M.closure Y) (hYE : Y ⊆ M.E := by aesop_mat) : M.Basis I Y

theorem Matroid.basis_union_iff_indep_closure {α : Type u_2} {M : Matroid α} {X I : Set α} : M.Basis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I

theorem Matroid.basis_iff_indep_closure {α : Type u_2} {M : Matroid α} {X I : Set α} : M.Basis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X

theorem Matroid.Basis.eq_of_closure_subset {α : Type u_2} {M : Matroid α} {X I J : Set α} (hI : M.Basis I X) (hJI : J ⊆ I) (hJ : X ⊆ M.closure J) : J = I

@[simp]

theorem Matroid.empty_basis_iff {α : Type u_2} {M : Matroid α} {X : Set α} : M.Basis ∅ X ↔ X ⊆ M.closure ∅

theorem Matroid.indep_iff_forall_not_mem_closure_diff {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})

theorem Matroid.indep_iff_forall_not_mem_closure_diff' {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})

An alternative version of Matroid.indep_iff_forall_not_mem_closure_diff where the hypothesis that I ⊆ M.E is contained in the RHS rather than the hypothesis.

theorem Matroid.Indep.not_mem_closure_diff_of_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : e ∉ M.closure (I \ {e})

theorem Matroid.indep_iff_forall_closure_diff_ne {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

theorem Matroid.Indep.closure_ssubset_closure {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJI : J ⊂ I) : M.closure J ⊂ M.closure I

theorem Matroid.indep_iff_forall_closure_ssubset_of_ssubset {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I

theorem Matroid.Indep.closure_diff_ssubset {α : Type u_2} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hX : (I ∩ X).Nonempty) : M.closure (I \ X) ⊂ M.closure I

theorem Matroid.Indep.closure_diff_singleton_ssubset {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : M.closure (I \ {e}) ⊂ M.closure I

theorem Matroid.mem_closure_insert {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∉ M.closure X) (hef : e ∈ M.closure (insert f X)) : f ∈ M.closure (insert e X)

theorem Matroid.closure_exchange {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∈ M.closure (insert f X) \ M.closure X) : f ∈ M.closure (insert e X) \ M.closure X

theorem Matroid.closure_exchange_iff {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} : e ∈ M.closure (insert f X) \ M.closure X ↔ f ∈ M.closure (insert e X) \ M.closure X

theorem Matroid.closure_insert_congr {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∈ M.closure (insert f X) \ M.closure X) : M.closure (insert e X) = M.closure (insert f X)

theorem Matroid.closure_diff_eq_self {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ M.closure (X \ Y)) : M.closure (X \ Y) = M.closure X

theorem Matroid.closure_diff_singleton_eq_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (h : e ∈ M.closure (X \ {e})) : M.closure (X \ {e}) = M.closure X

theorem Matroid.subset_closure_diff_iff_closure_eq {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ X) (hY : Y ⊆ M.E := by aesop_mat) : Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X

theorem Matroid.mem_closure_diff_singleton_iff_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ X) (heE : e ∈ M.E := by aesop_mat) : e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X

theorem Matroid.ext_closure {α : Type u_2} {M₁ M₂ : Matroid α} (h : ∀ (X : Set α), M₁.closure X = M₂.closure X) : M₁ = M₂

structure Matroid.Spanning {α : Type u_2} (M : Matroid α) (S : Set α) : Prop

A set is spanning in M if its closure is equal to M.E, or equivalently if it contains a base of M.

• closure_eq : M.closure S = M.E
• subset_ground : S ⊆ M.E

theorem Matroid.spanning_iff {α : Type u_2} (M : Matroid α) (S : Set α) : M.Spanning S ↔ M.closure S = M.E ∧ S ⊆ M.E

theorem Matroid.spanning_iff_closure_eq {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ M.closure S = M.E

@[simp]

theorem Matroid.closure_spanning_iff {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning (M.closure S) ↔ M.Spanning S

theorem Matroid.spanning_iff_ground_subset_closure {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ M.E ⊆ M.closure S

theorem Matroid.not_spanning_iff_closure_ssubset {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : ¬M.Spanning S ↔ M.closure S ⊂ M.E

theorem Matroid.Spanning.superset {α : Type u_2} {M : Matroid α} {S T : Set α} (hS : M.Spanning S) (hST : S ⊆ T) (hT : T ⊆ M.E := by aesop_mat) : M.Spanning T

theorem Matroid.Spanning.closure_eq_of_superset {α : Type u_2} {M : Matroid α} {S T : Set α} (hS : M.Spanning S) (hST : S ⊆ T) : M.closure T = M.E

theorem Matroid.Spanning.union_left {α : Type u_2} {M : Matroid α} {X S : Set α} (hS : M.Spanning S) (hX : X ⊆ M.E := by aesop_mat) : M.Spanning (S ∪ X)

theorem Matroid.Spanning.union_right {α : Type u_2} {M : Matroid α} {X S : Set α} (hS : M.Spanning S) (hX : X ⊆ M.E := by aesop_mat) : M.Spanning (X ∪ S)

theorem Matroid.Base.spanning {α : Type u_2} {M : Matroid α} {B : Set α} (hB : M.Base B) : M.Spanning B

theorem Matroid.ground_spanning {α : Type u_2} (M : Matroid α) : M.Spanning M.E

theorem Matroid.Base.spanning_of_superset {α : Type u_2} {M : Matroid α} {X B : Set α} (hB : M.Base B) (hBX : B ⊆ X) (hX : X ⊆ M.E := by aesop_mat) : M.Spanning X

theorem Matroid.spanning_iff_exists_base_subset' {α : Type u_2} {M : Matroid α} {S : Set α} : M.Spanning S ↔ (∃ (B : Set α), M.Base B ∧ B ⊆ S) ∧ S ⊆ M.E

A version of Matroid.spanning_iff_exists_base_subset in which the S ⊆ M.E condition appears in the RHS of the equivalence rather than as a hypothesis.

theorem Matroid.spanning_iff_exists_base_subset {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ ∃ (B : Set α), M.Base B ∧ B ⊆ S

theorem Matroid.Spanning.exists_base_subset {α : Type u_2} {M : Matroid α} {S : Set α} (hS : M.Spanning S) : ∃ (B : Set α), M.Base B ∧ B ⊆ S

theorem Matroid.coindep_iff_compl_spanning {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Coindep I ↔ M.Spanning (M.E \ I)

theorem Matroid.spanning_iff_compl_coindep {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ M.Coindep (M.E \ S)

theorem Matroid.Coindep.compl_spanning {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Coindep I) : M.Spanning (M.E \ I)

theorem Matroid.coindep_iff_closure_compl_eq_ground {α : Type u_2} {M : Matroid α} {X : Set α} (hK : X ⊆ M.E := by aesop_mat) : M.Coindep X ↔ M.closure (M.E \ X) = M.E

theorem Matroid.Coindep.closure_compl {α : Type u_2} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : M.closure (M.E \ X) = M.E

theorem Matroid.Indep.base_of_spanning {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hIs : M.Spanning I) : M.Base I

theorem Matroid.Spanning.base_of_indep {α : Type u_2} {M : Matroid α} {I : Set α} (hIs : M.Spanning I) (hI : M.Indep I) : M.Base I

theorem Matroid.ext_spanning {α : Type u_2} {M M' : Matroid α} (h : M.E = M'.E) (hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S) : M = M'