Matroid.Finite.ground_finite
theorem Matroid.Finite.ground_finite : ∀ {α : Type u_1} {M : Matroid α} [self : M.Finite], M.E.Finite
This theorem states that for any type `α` and any Matroid `M` of type `α`, given a condition where `M` is finite (denoted by `M.Finite`), the ground set `E` of the Matroid `M` is also finite (`M.E.Finite`). In other words, if a Matroid is finite, then its ground set is also finite.
More concisely: If `M` is a finite matroid of type `α`, then its ground set `M.E` is also finite.
|
Matroid.exists_base
theorem Matroid.exists_base : ∀ {α : Type u_1} (self : Matroid α), ∃ B, self.Base B
This theorem states that for any given Matroid of type `α`, there exists at least one `Base`. In other words, for each and every Matroid, we can find a `Base` that belongs to it.
More concisely: Every matroid has at least one base.
|
Matroid.Indep.exists_insert_of_not_mem_maximals
theorem Matroid.Indep.exists_insert_of_not_mem_maximals :
∀ {α : Type u_1} (M : Matroid α) ⦃I B : Set α⦄,
M.Indep I →
I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I} →
B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I} → ∃ x ∈ B \ I, M.Indep (insert x I)
This theorem is about independent sets in a Matroid. In particular, it states that for any type `α`, given a Matroid `M` and two sets `I` and `B`, if `I` is an independent set in the Matroid and `I` is not a maximal independent set according to the subset relation, and `B` is a maximal independent set according to the subset relation, then there exists an element `x` in the set difference `B \ I` such that the set resulting from inserting `x` into `I` is also an independent set in `M`. This theorem is equivalent to the augmentation axiom for independent sets in Matroid theory, which asserts that if one independent set is smaller than another, then there's an element in the larger set that can be added to the smaller one to also create an independent set.
More concisely: Given a Matroid `M` and independent sets `I` and `B` where `I` is proper subset of `B` and `B` is maximal, there exists an element `x` in `B \ I` such that `I ∪ {x}` is also an independent set in `M`.
|
Matroid.Base.eq_of_subset_base
theorem Matroid.Base.eq_of_subset_base :
∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.Base B₁ → M.Base B₂ → B₁ ⊆ B₂ → B₁ = B₂
This theorem establishes a property of bases in a matroid. In particular, for any type `α` and any matroid `M` over `α`, if `B₁` and `B₂` are both sets of `α` and are both bases in `M`, then if `B₁` is a subset of `B₂`, it must be the case that `B₁` is equal to `B₂`. This theorem is useful in understanding the structure and properties of bases in matroids.
More concisely: In any matroid, if two bases have non-empty intersection, then they are equal.
|
Matroid.existsMaximalSubsetProperty_indep
theorem Matroid.existsMaximalSubsetProperty_indep :
∀ {α : Type u_1} (M : Matroid α), ∀ X ⊆ M.E, Matroid.ExistsMaximalSubsetProperty M.Indep X
The theorem `Matroid.existsMaximalSubsetProperty_indep` states that for any type `α` and any matroid `M` on this type, if `X` is a subset of the ground set of the matroid, then `X` has the maximal subset property with respect to the independence predicate of the matroid. In other words, for any independent subset `I` of `X`, there exists a maximal independent subset `Y` of the ground set of the matroid such that `I` is contained in `Y` and `Y` is contained in `X`. This property is a key axiom in the definition of a matroid.
More concisely: For any matroid and any of its subset, there exists a maximal independent subset contained within it.
|
Matroid.Finitary.indep_of_forall_finite
theorem Matroid.Finitary.indep_of_forall_finite :
∀ {α : Type u_1} {M : Matroid α} [self : M.Finitary] (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I := by
sorry
This theorem is about the independence property in a matroid structure. In the context of a given matroid `M` on a type `α`, a set `I` of type `α` is said to be independent if every finite subset `J` of `I` is independent. That is, for all subsets `J` that are contained in `I` and are finite, if all these subsets `J` satisfy the independence property in the matroid `M`, then the set `I` itself is also independent in the matroid `M`.
More concisely: If every finite subset of a set `I` in a matroid `M` is independent, then set `I` itself is independent in matroid `M`.
|
Matroid.Indep.subset
theorem Matroid.Indep.subset : ∀ {α : Type u_1} {M : Matroid α} {J I : Set α}, M.Indep J → I ⊆ J → M.Indep I
This theorem states that for any type `α` and for any Matroid `M` of type `α`, if `J` and `I` are sets from the type `α`, and if `J` is an independent set in the matroid `M`, then if `I` is a subset of `J`, `I` is also an independent set in the matroid `M`. Here, `M.Indep J` and `M.Indep I` refer to the independence of the sets `J` and `I` in the matroid `M` respectively, and `I ⊆ J` denotes that `I` is a subset of `J`.
More concisely: If `M` is a matroid over type `α`, `J` is an independent set in `M`, and `I ⊆ J`, then `I` is also an independent set in `M`.
|
Matroid.basis_iff
theorem Matroid.basis_iff :
∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
autoParam (X ⊆ M.E) _auto✝ →
(M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J)
The theorem `Matroid.basis_iff` states that for any type `α` and a matroid `M` on that type, as well as for any two sets `X` and `I` of that type, given that `X` is a subset of the ground set of `M` (assumed automatically), a set `I` is a basis of `X` in `M` if and only if `I` is independent in `M`, `I` is a subset of `X`, and for any other set `J` which is independent and a subset of `X`, if `I` is also a subset of `J`, then `I` and `J` must be the same set. In short, a basis is an independent set within `X` that cannot be further expanded by any other independent set within `X`.
More concisely: A set is a basis of a matroid if and only if it is an independent subset that is not a proper subset of any other independent subset.
|
Matroid.Dep.not_indep
theorem Matroid.Dep.not_indep : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D → ¬M.Indep D
This theorem states that for any type `α`, any `Matroid` `M` over `α`, and any set `D` of `α`, if `D` is a dependent set in `M` then `D` cannot be an independent set in `M`. In other words, a set cannot be both dependent and independent in the context of the same matroid.
More concisely: In a matroid, no set can be both dependent and independent.
|
Matroid.Indep.subset_basis_of_subset
theorem Matroid.Indep.subset_basis_of_subset :
∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
M.Indep I → I ⊆ X → autoParam (X ⊆ M.E) _auto✝ → ∃ J, M.Basis J X ∧ I ⊆ J
This theorem states that for any type `α`, given a matroid `M` of type `α`, and two sets `I` and `X` of type `α`, if `I` is independent within the matroid `M` and `I` is a subset of `X`, with `X` being a subset of the matroid's set `E` (the latter is an automatic parameter indicated by `autoParam`), there exists a set `J` such that `J` is a basis of `X` within the matroid `M` and `I` is also a subset of `J`.
More concisely: For any matroid M over type α, if I is an independent subset of X within M and I is a subset of X, then there exists a basis J of X in M containing I.
|
Matroid.Basis.mem_of_insert_indep
theorem Matroid.Basis.mem_of_insert_indep :
∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α}, M.Basis I X → e ∈ X → M.Indep (insert e I) → e ∈ I := by
sorry
The theorem `Matroid.Basis.mem_of_insert_indep` states that for any type `α`, any matroid `M` over `α`, any two sets `I` and `X` of `α`, and any element `e` of type `α`, if `I` is a basis of `X` in `M`, `e` is an element of `X`, and the set obtained by inserting `e` into `I` is independent in `M`, then `e` is an element of `I`. In other words, in a matroid, if we have an independent set that is also a basis for another set, and an element from that other set can be added without destroying independence, then that element was already in the original basis.
More concisely: If `I` is a basis of a matroid `M` over `α`, `e` is an element of `X` in `M` with `I ∣ X` independent, then `e` is an element of `I`.
|
Matroid.Basis.eq_of_subset_indep
theorem Matroid.Basis.eq_of_subset_indep :
∀ {α : Type u_1} {M : Matroid α} {I X J : Set α}, M.Basis I X → M.Indep J → I ⊆ J → J ⊆ X → I = J
The theorem `Matroid.Basis.eq_of_subset_indep` states that for any type `α`, given a Matroid `M` on `α` and sets `I`, `X`, and `J` of type `α`, if `I` is a basis of `X` in `M`, and `J` is independent in `M`, and `I` is a subset of `J`, and `J` is a subset of `X`, then `I` must be equal to `J`. In other words, in the context of a matroid, any independent set `J` that is a subset of a set `X` and also contains a basis `I` of `X` must be the same as `I`.
More concisely: If `I` is a basis of a set `X` in a matroid `M`, and `J` is an independent subset of `X` that contains `I`, then `I` equals `J`.
|
Matroid.Base.indep
theorem Matroid.Base.indep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.Base B → M.Indep B
This theorem states that for any type `α`, any Matroid `M` defined on this type, and any set `B` of elements of type `α`, if `B` is a base of the Matroid `M` (`M.Base B`), then `B` is also an independent set in `M` (`M.Indep B`). In other words, every base of a Matroid is also an independent set in the Matroid.
More concisely: For any Matroid M over type α, if B is a base of M then B is an independent set in M.
|
Matroid.Base.exchange
theorem Matroid.Base.exchange :
∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α},
M.Base B₁ → M.Base B₂ → e ∈ B₁ \ B₂ → ∃ y ∈ B₂ \ B₁, M.Base (insert y (B₁ \ {e}))
The Base Exchange Theorem in Matroid states that for any type `α` and any matroid `M` of type `α`, and for any two sets `B₁` and `B₂` of type `α`, and an element `e` of type `α`, if `B₁` and `B₂` are both bases of `M` and if `e` is an element of the difference of `B₁` and `B₂`, then there exists an element `y` in the difference of `B₂` and `B₁` such that the set obtained by inserting `y` into the difference of `B₁` and the singleton set `{e}` is also a base of `M`.
In simpler terms, if `B₁` and `B₂` are bases of the same matroid and `e` is in `B₁` but not in `B₂`, then there's an element `y` in `B₂` (but not in `B₁`) such that if we remove `e` from `B₁` and add `y`, the resulting set is still a base of the matroid. This theorem is a cornerstone in the theory of matroids, underlying the concept of bases exchangeability.
More concisely: If two bases of a matroid differ by exactly one element, then there exists an element in each base that can be exchanged to obtain another base.
|
Matroid.Base.finite
theorem Matroid.Base.finite : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} [inst : M.FiniteRk], M.Base B → B.Finite
The theorem `Matroid.Base.finite` states that for any type `α`, any matroid `M` of type `α`, and any set `B` of type `α`, given an instance where the rank of the matroid `M` is finite (`Matroid.FiniteRk M`), if `B` is a base of the matroid `M` (`M.Base B`), then the set `B` is finite (`Set.Finite B`). Essentially, this theorem asserts that every base of a matroid with finite rank is a finite set.
More concisely: If `M` is a matroid of finite rank over type `α`, then any base `B` of `M` is a finite set.
|
Matroid.RkPos.empty_not_base
theorem Matroid.RkPos.empty_not_base : ∀ {α : Type u_1} {M : Matroid α} [self : M.RkPos], ¬M.Base ∅
This theorem states that the empty set is not a base in any matroid. More specifically, for any given type `α` and any given matroid `M` defined on `α`, if the rank function of `M` is positive, then the empty set is not a base of the matroid `M`.
More concisely: For any matroid M on type α with positive rank function, the empty set is not a base.
|
Matroid.Basis.subset_ground
theorem Matroid.Basis.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Basis I X → X ⊆ M.E
This theorem is stating that for any type `α` and a `Matroid` `M` of that type, and any two sets `I` and `X` of type `α`, if `I` is a basis of `X` in `M` (denoted as `M.Basis I X`), then `X` is a subset of the ground set of `M` (denoted as `M.E`). In mathematical terms, if $I$ is a basis of $X$ in a matroid $M$, it implies that $X$ is included in the ground set of $M$.
More concisely: If `α` is a type and `M` is a Matroid of type `α`, then for any sets `I` and `X` of type `α` with `I` being a basis of `X` in `M`, we have `X ⊆ M.E`.
|
Matroid.InfiniteRk.exists_infinite_base
theorem Matroid.InfiniteRk.exists_infinite_base :
∀ {α : Type u_1} {M : Matroid α} [self : M.InfiniteRk], ∃ B, M.Base B ∧ B.Infinite
This theorem states that for any type `α` and any `Matroid` `M` of that type with infinite rank, there exists a `Base` `B` of `M` that is infinite. In other words, given a mathematical structure called a matroid that has infinite rank, there is always an infinite base within that matroid.
More concisely: For any infinite rank Matroid `M` over type `α`, there exists an infinite base `B` for `M`.
|
Matroid.Nonempty.ground_nonempty
theorem Matroid.Nonempty.ground_nonempty : ∀ {α : Type u_1} {M : Matroid α} [self : M.Nonempty], M.E.Nonempty := by
sorry
This theorem states that for any given matroid 'M' of an arbitrary type 'α', if the matroid is nonempty, then the ground set 'E' of the matroid is also nonempty. In simpler terms, if a matroid has at least one element, then its set of all elements also contains at least one element. This theorem is foundational to the structure of matroids in the field of combinatorial optimization.
More concisely: If M is a nonempty matroid, then its ground set E is nonempty.
|
Matroid.Basis.subset
theorem Matroid.Basis.subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Basis I X → I ⊆ X
This theorem states that for any type `α`, any matroid `M` over `α`, and any sets `I` and `X` of elements of type `α`, if `I` is a basis of `X` in `M`, then `I` is a subset of `X`. In other words, every element in the basis `I` is also an element in the set `X`.
More concisely: For any matroid M over type α and any sets I (a basis of X in M) and X of elements of α, I is a subset of X.
|
Matroid.Indep.exists_base_superset
theorem Matroid.Indep.exists_base_superset :
∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∃ B, M.Base B ∧ I ⊆ B
The theorem `Matroid.Indep.exists_base_superset` states that for any type `α`, any matroid `M` on `α`, and any independent set `I` in `M`, there exists a base `B` of `M` such that `I` is a subset of `B`. In other words, every independent set in a matroid can be extended to form a base of the matroid.
More concisely: For every matroid and every independent set, there exists a base containing that set.
|
Matroid.Indep.basis_self
theorem Matroid.Indep.basis_self : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.Basis I I
This theorem states that for any type `α`, any Matroid `M` of that type, and any set `I` of that type, if `I` is an independent set in `M` (`M.Indep I`), then `I` is a basis for itself in `M` (`M.Basis I I`). In other words, in the context of matroid theory, an independent set within a matroid is also a basis of itself within that matroid.
More concisely: For any matroid M and any independent set I in its type α, I is a basis of I in M.
|
Matroid.FiniteRk.exists_finite_base
theorem Matroid.FiniteRk.exists_finite_base :
∀ {α : Type u_1} {M : Matroid α} [self : M.FiniteRk], ∃ B, M.Base B ∧ B.Finite
This theorem states that for any type `α` and any Matroid `M` of this type `α`, under the condition that `M` is of finite rank (as indicated by `[self : M.FiniteRk]`), there exists a base `B` that is finite and belongs to the Matroid `M`. In other words, in the context of a finite rank Matroid, we can always find a finite base.
More concisely: For any finite rank Matroid `M` over type `α`, there exists a finite base in `M`.
|
Matroid.Base.finiteRk_of_finite
theorem Matroid.Base.finiteRk_of_finite :
∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.Base B → B.Finite → M.FiniteRk
This theorem asserts that, for any type `α`, given a matroid `M` over that type and a set `B` of that type, if `B` is a base of the matroid `M` and `B` is a finite set, then the rank of that matroid `M` is finite. In other words, if we have a finite base for a matroid, it implies that the rank of the matroid is finite. Here, 'base' and 'rank' refer to the mathematical concepts from the theory of matroids.
More concisely: If `M` is a matroid over type `α`, `B` is a finite base of `M`, then the rank of `M` is finite.
|
Matroid.Basis.union_basis_union
theorem Matroid.Basis.union_basis_union :
∀ {α : Type u_1} {M : Matroid α} {I X J Y : Set α},
M.Basis I X → M.Basis J Y → M.Indep (I ∪ J) → M.Basis (I ∪ J) (X ∪ Y)
This theorem, named "union_basis_union", pertains to the context of Matroids in mathematics. It states that for any type `α`, and any `Matroid` named `M` of that type, if `I`,`X`,`J`, and `Y` are all sets of `α`, and if `I` and `X` form a basis of `M` (`M.Basis I X`), as well as `J` and `Y` (`M.Basis J Y`), and if `I union J` is independent (`M.Indep (I ∪ J)`), then `I union J` and `X union Y` also form a basis of `M` (`M.Basis (I ∪ J) (X ∪ Y)`). Thus, it provides a condition under which the union of two bases in a Matroid yields another valid basis.
More concisely: If two sets are bases of a matroid and their union is independent, then their union is also a basis.
|
Matroid.Indep.exists_insert_of_not_base
theorem Matroid.Indep.exists_insert_of_not_base :
∀ {α : Type u_1} {M : Matroid α} {I B : Set α},
M.Indep I → ¬M.Base I → M.Base B → ∃ e ∈ B \ I, M.Indep (insert e I)
This theorem states that for any type `α` and any given `Matroid` `M` over `α`, if `I` and `B` are sets of elements in `α` with `I` being independent in `M` but not a basis, and `B` being a basis, then there exists an element `e` from the set `B` distinct from `I` such that inserting `e` into `I` still results in an independent set in `M`. In other words, we can always add a new element from a basis to an independent set which is not yet a basis, without violating the independence property.
More concisely: For any matroid M over type α and any independent set I that is not a basis, there exists an element e in basis B such that I ∪ {e} remains independent in M.
|
Matroid.Base.encard_diff_comm
theorem Matroid.Base.encard_diff_comm :
∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.Base B₁ → M.Base B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard := by
sorry
The theorem `Matroid.Base.encard_diff_comm` states that for any type `α`, any matroid `M` on `α`, and any two base sets `B₁` and `B₂` of the matroid, if `B₁` and `B₂` are both bases of the matroid, then the cardinality of the set difference `B₁ \ B₂` (elements in `B₁` but not in `B₂`) is equal to the cardinality of the set difference `B₂ \ B₁` (elements in `B₂` but not in `B₁`). In other words, the sizes of the unique elements in each base with respect to the other are the same.
More concisely: For any matroid on a type `α`, if two bases have the same number of unique elements with respect to each other, then their set differences have equal cardinalities.
|
Matroid.basis_iff'
theorem Matroid.basis_iff' :
∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
M.Basis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
This theorem states that for any type `α`, a `Matroid` `M` on `α`, and sets `I` and `X` of `α`, the set `I` is a basis of `X` in `M` if and only if `I` is independent in `M`, `I` is a subset of `X`, and for any independent set `J` of `α` in `M` such that `I` is a subset of `J` and `J` is a subset of `X`, `I` must equal `J`. Furthermore, `X` is a subset of the elements of `M`.
More concisely: A set `I` is a basis of a matroid `M` over a type `α` if and only if it is independent in `M`, is a subset of `X` in `M`, and for any independent `J` with `I` and `J` both subsets of `X`, `I` equals `J`.
|
Matroid.ExchangeProperty.encard_base_eq
theorem Matroid.ExchangeProperty.encard_base_eq :
∀ {α : Type u_1} {Base : Set α → Prop},
Matroid.ExchangeProperty Base → ∀ {B₁ B₂ : Set α}, Base B₁ → Base B₂ → B₁.encard = B₂.encard
The theorem `Matroid.ExchangeProperty.encard_base_eq` states that for any given type `α` and property `Base` defined on sets of type `α`, if this property satisfies the matroid exchange property, then any two sets `B₁` and `B₂` which satisfy the `Base` property will have the same `ℕ∞`-cardinality. In simpler terms, in a family of sets with the exchange property, any two sets that satisfy the base property will have the same size.
More concisely: If `α` is a type with `Base` being a property on sets satisfying the matroid exchange property, then for any two sets `B₁` and `B₂` of type `α` with the property `Base`, their `ℕ∞`-cardinalities are equal.
|
Matroid.ExchangeProperty.encard_diff_eq
theorem Matroid.ExchangeProperty.encard_diff_eq :
∀ {α : Type u_1} {Base : Set α → Prop},
Matroid.ExchangeProperty Base → ∀ {B₁ B₂ : Set α}, Base B₁ → Base B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard
The theorem `Matroid.ExchangeProperty.encard_diff_eq` states that for any type `α` and any predicate `Base` on sets of `α` that satisfies the exchange property, for any two sets `B₁` and `B₂` such that `Base B₁` and `Base B₂` hold, the `ℕ∞`-cardinality (essentially, the size) of the difference `B₁ \ B₂` is equal to the `ℕ∞`-cardinality of the difference `B₂ \ B₁`. This means that the number of elements unique to each of the two sets is the same, when we have a family of sets with the exchange property.
More concisely: For any type `α` and predicate `Base` on sets of `α` satisfying the exchange property, the size of `Base B₁ ∖ Base B₂` equals the size of `Base B₂ ∖ Base B₁`.
|
Matroid.subset_ground
theorem Matroid.subset_ground : ∀ {α : Type u_1} (self : Matroid α) (B : Set α), self.Base B → B ⊆ self.E
The theorem `Matroid.subset_ground` states that for any type `α`, for any matroid defined on that type, and for any set `B` of that type that forms a base of the matroid, the set `B` is a subset of the ground set `E` of the matroid. In other words, every base of a matroid is always contained within the matroid's ground set.
More concisely: For any matroid and any of its base sets, that set is a subset of the matroid's ground set.
|
Matroid.Base.subset_ground
theorem Matroid.Base.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.Base B → B ⊆ M.E
This theorem states that for any type `α`, any `Matroid` `M` on this type, and any set `B` of this type, if `B` is a base of the matroid `M`, then `B` is a subset of the ground set `E` of the matroid `M`. In other words, every base of a matroid is always a subset of the ground set of the matroid.
More concisely: For any matroid M on type α, any base B of M is a subset of M's ground set E.
|
Matroid.Basis.indep
theorem Matroid.Basis.indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Basis I X → M.Indep I
This theorem states that for any type `α`, any `Matroid` `M` over `α`, and any two sets `I` and `X` of type `α`, if `X` is a basis of `I` under matroid `M` (denoted as `M.Basis I X`), then `I` is an independent set under matroid `M` (denoted as `M.Indep I`).
In other words, this theorem establishes that in a matroid structure, all basis sets are independent.
More concisely: In a matroid, every basis is an independent set.
|
Matroid.empty_indep
theorem Matroid.empty_indep : ∀ {α : Type u_1} (M : Matroid α), M.Indep ∅
This theorem states that for any given matroid `M` over a type `α`, the empty set is independent in `M`. In other words, in the context of matroids, which are a generalization of graphs, vectors, and other mathematical structures, this theorem guarantees that no matter what specific matroid we are considering, an empty set will always be considered independent.
More concisely: In any matroid, the empty set is an independent set.
|
Matroid.Base.eq_exchange_of_diff_eq_singleton
theorem Matroid.Base.eq_exchange_of_diff_eq_singleton :
∀ {α : Type u_1} {M : Matroid α} {B B' : Set α} {e : α},
M.Base B → M.Base B' → B \ B' = {e} → ∃ f ∈ B' \ B, B' = insert f B \ {e}
The theorem `Matroid.Base.eq_exchange_of_diff_eq_singleton` states that for all types `α` and all Matroids `M` of that type, given two sets `B` and `B'` of that type and an element `e` of the type, if `B` and `B'` are both bases of the Matroid `M` and the difference of the two sets `B` and `B'` is a singleton set containing only the element `e`, then there exists an element `f` in the difference of `B'` and `B` such that `B'` can be obtained from `B` by inserting `f` and removing `e`. Essentially, this theorem describes a property of matroid bases stating that if two bases differ by a single element, they can be transformed into each other by a simple exchange operation.
More concisely: For all types `α` and Matroids `M` of type `α`, if `B` and `B'` are bases of `M`, and `B` and `B'` differ by a singleton set containing an element `e`, then there exists an element `f` such that `B'` is obtained from `B` by exchanging `e` with `f`.
|
Matroid.base_exchange
theorem Matroid.base_exchange : ∀ {α : Type u_1} (self : Matroid α), Matroid.ExchangeProperty self.Base
The theorem `base_exchange` is a property of a matroid, which says that for any two bases `B` and `B'` of the matroid, and for any element `e` in the difference set `B \ B'` (i.e., the set of elements that are in `B` but not in `B'`), there exists some element `f` in the difference set `B' \ B` (i.e., the set of elements that are in `B'` but not in `B`) such that the set obtained by removing `e` from `B` and adding `f` to `B` is also a base of the matroid. This property is known as the **base exchange property** of a matroid.
More concisely: For any two bases of a matroid, there exists an element in the difference between them such that removing it from one and adding it to the other results in another base.
|
Matroid.Base.eq_of_subset_indep
theorem Matroid.Base.eq_of_subset_indep :
∀ {α : Type u_1} {M : Matroid α} {B I : Set α}, M.Base B → M.Indep I → B ⊆ I → B = I
This theorem states that for any type `α`, given a Matroid `M` on `α` and two sets `B` and `I` of elements of type `α`, if `B` is a base of `M`, `I` is independent in `M`, and `B` is a subset of `I`, then `B` and `I` are equal. In other words, in the context of a matroid, an independent set that contains a base must be equal to that base.
More concisely: If `M` is a matroid on type `α`, `B` is a base of `M`, `I` is an independent set of `M`, and `B` is a subset of `I`, then `B = I`.
|
Matroid.Indep.subset_ground
theorem Matroid.Indep.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I ⊆ M.E
This theorem states that for any type `α`, any Matroid `M` defined over this type, and any Set `I` of elements of this type, if `I` is an independent set in the Matroid `M` (denoted by `M.Indep I`), then `I` is a subset of the ground set of the Matroid `M` (denoted by `M.E`). In other words, all independent sets in a matroid are subsets of the matroid's ground set.
More concisely: For any matroid M and its ground set E, any independent set I of M is a subset of E.
|
Matroid.ExchangeProperty.antichain
theorem Matroid.ExchangeProperty.antichain :
∀ {α : Type u_1} {Base : Set α → Prop},
Matroid.ExchangeProperty Base → ∀ {B B' : Set α}, Base B → Base B' → B ⊆ B' → B = B'
The theorem states that if a family of sets possesses the exchange property, it forms an antichain. In other words, given any type 'α' and a family of sets 'Base' of that type, if 'Base' satisfies the exchange property, then for any two sets 'B' and 'B'' in 'Base', if 'B' is a subset of 'B'', then 'B' must be equal to 'B''. This implies that in this family of sets, no set is a proper subset of another, which is the definition of an antichain.
More concisely: If a family of sets has the exchange property, then it is an antichain (no set is a proper subset of another).
|
Matroid.base_iff_maximal_indep
theorem Matroid.base_iff_maximal_indep :
∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.Base B ↔ M.Indep B ∧ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I := by
sorry
This theorem states that for any type `α` and any `Matroid` `M` defined on that type, a set `B` is a base of the matroid if and only if `B` is independent and for any independent set `I`, if `B` is a subset of `I`, then `B` must be equal to `I`. In other words, a base in a matroid is a maximal independent set — it is independent, and any larger independent set must be the same set.
More concisely: A set is a base of a matroid if and only if it is maximal among the independent sets.
|
Matroid.maximality
theorem Matroid.maximality :
∀ {α : Type u_1} (self : Matroid α),
∀ X ⊆ self.E, Matroid.ExistsMaximalSubsetProperty (fun x => ∃ B, self.Base B ∧ x ⊆ B) X
This theorem states that for any given Matroid of type `α`, and for any subset `X` of the Matroid's set of elements `E`, if `X` is contained within a base of the Matroid, then there exists a maximal subset of `X` that also is contained within a base. In other words, any subset of the Matroid that is within a base is also within a maximal subset of the Matroid that itself is within a base. This is a property of the Matroid's structure.
More concisely: If a subset of the elements of a matroid is contained in a base, then it is contained in some maximal base.
|