Matroid.existsMaximalSubsetProperty_of_bdd
theorem Matroid.existsMaximalSubsetProperty_of_bdd :
∀ {α : Type u_1} {P : Set α → Prop},
(∃ n, ∀ (Y : Set α), P Y → Y.encard ≤ ↑n) → ∀ (X : Set α), Matroid.ExistsMaximalSubsetProperty P X
This theorem states that for any type `α` and predicate `P` on set of elements of that type, if there exists an absolute upper bound on the size of a set satisfying the predicate `P`, then the maximal subset property always holds for any set `X`. In terms of matroids, if the size of the set satisfying a condition `P` is bounded, every subset of a given set `X` satisfying `P` is contained in a maximal subset of `X` satisfying `P`.
More concisely: If a predicate `P` on a type `α` has a bounded maximum set size, then every subset of any set `X` satisfying `P` is contained in some maximal subset of `X` satisfying `P`.
|
Mathlib.Data.Matroid.IndepAxioms._auxLemma.15
theorem Mathlib.Data.Matroid.IndepAxioms._auxLemma.15 :
∀ {α : Type u_1} {M : IndepMatroid α} {I : Set α}, M.matroid.Indep I = M.Indep I
The theorem `Mathlib.Data.Matroid.IndepAxioms._auxLemma.15` states that for any type `α`, any independent matroid `M` of type `α`, and any set `I` of elements of type `α`, the independence property of the matroid derived from `M` by the `IndepMatroid.matroid` function applied to `I` is equal to the independence property of `M` applied to `I`. In simpler terms, it says that the independence property is preserved when we convert an independent matroid to a matroid using the `IndepMatroid.matroid` function.
More concisely: For any type `α`, any independent matroid `M` over `α`, and any set `I` of elements from `α`, the matroid `IndepMatroid.matroid M I` is independent if and only if `I` is independent in `M`.
|
IndepMatroid.ofFinset_indep'
theorem IndepMatroid.ofFinset_indep' :
∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
(indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
(subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) {I : Set α},
(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
∀ (J : Finset α), ↑J ⊆ I → Indep J
This theorem, named `IndepMatroid.ofFinset_indep'`, states that for any type `α` with decidable equality, given a set `E` of `α`, a property `Indep` on finite subsets of `α` (represented as `Finset α`), and specific conditions on `Indep` such as it holds for empty set, it is preserved under taking subset, there exists an element in a larger independent set which can be added to a smaller independent set maintaining the independence, and every independent set is a subset of `E`, then for any subset `I` of `α`, the independence property of `I` in the matroid constructed from `E` and `Indep` (by `IndepMatroid.ofFinset`) is equivalent to `Indep` holding for all finite subsets `J` of `α` which are contained in `I`.
More concisely: Given a type `α` with decidable equality, a set `E` of `α`, a property `Indep` on finite subsets of `α`, and if `Indep` holds for empty sets, is preserved under taking subsets, and every independent set is a subset of `E`, then for any subset `I` of `α`, the sets `{J : Finset α | J ⊆ I → Indep J}` and `{S : Finset α | S ⊆ I → IndepMatroid.ofFinset E S}` are equal.
|