# Matroids #

A `Matroid` is a structure that combinatorially abstracts the notion of linear independence and dependence; matroids have connections with graph theory, discrete optimization, additive combinatorics and algebraic geometry. Mathematically, a matroid `M` is a structure on a set `E` comprising a collection of subsets of `E` called the bases of `M`, where the bases are required to obey certain axioms.

This file gives a definition of a matroid `M` in terms of its bases, and some API relating independent sets (subsets of bases) and the notion of a basis of a set `X` (a maximal independent subset of `X`).

## Main definitions #

- a `Matroid α` on a type `α` is a structure comprising a 'ground set' and a suitably behaved 'base' predicate.

Given `M : Matroid α` ...

- `M.E` denotes the ground set of `M`, which has type `Set α`

- For `B : Set α`, `M.IsBase B` means that `B` is a base of `M`.

- For `I : Set α`, `M.Indep I` means that `I` is independent in `M` (that is, `I` is contained in a base of `M`).

- For `D : Set α`, `M.Dep D` means that `D` is contained in the ground set of `M` but isn't independent.

- For `I : Set α` and `X : Set α`, `M.IsBasis I X` means that `I` is a maximal independent subset of `X`.

- `M.Finite` means that `M` has finite ground set.

- `M.Nonempty` means that the ground set of `M` is nonempty.

- `RankFinite M` means that the bases of `M` are finite.

- `RankInfinite M` means that the bases of `M` are infinite.

- `RankPos M` means that the bases of `M` are nonempty.

- `Finitary M` means that a set is independent if and only if all its finite subsets are independent.

- `aesop_mat` : a tactic designed to prove `X ⊆ M.E` for some set `X` and matroid `M`.

## Implementation details #

There are a few design decisions worth discussing.

### Finiteness #

The first is that our matroids are allowed to be infinite. Unlike with many mathematical structures, this isn't such an obvious choice. Finite matroids have been studied since the 1930's, and there was never controversy as to what is and isn't an example of a finite matroid - in fact, surprisingly many apparently different definitions of a matroid give rise to the same class of objects.

However, generalizing different definitions of a finite matroid to the infinite in the obvious way (i.e. by simply allowing the ground set to be infinite) gives a number of different notions of 'infinite matroid' that disagree with each other, and that all lack nice properties. Many different competing notions of infinite matroid were studied through the years; in fact, the problem of which definition is the best was only really solved in 2013, when Bruhn et al. [2] showed that there is a unique 'reasonable' notion of an infinite matroid (these objects had previously defined by Higgs under the name 'B-matroid'). These are defined by adding one carefully chosen axiom to the standard set, and adapting existing axioms to not mention set cardinalities; they enjoy nearly all the nice properties of standard finite matroids.

Even though at least 90% of the literature is on finite matroids, B-matroids are the definition we use, because they allow for additional generality, nearly all theorems are still true and just as easy to state, and (hopefully) the more general definition will prevent the need for a costly future refactor. The disadvantage is that developing API for the finite case is harder work (for instance, it is harder to prove that something is a matroid in the first place, and one must deal with `ℕ∞` rather than `ℕ`). For serious work on finite matroids, we provide the typeclasses `[M.Finite]` and `[RankFinite M]` and associated API.

### Cardinality #

Just as with bases of a vector space, all bases of a finite matroid `M` are finite and have the same cardinality; this cardinality is an important invariant known as the 'rank' of `M`. For infinite matroids, bases are not in general equicardinal; in fact the equicardinality of bases of infinite matroids is independent of ZFC [3]. What is still true is that either all bases are finite and equicardinal, or all bases are infinite. This means that the natural notion of 'size' for a set in matroid theory is given by the function `Set.encard`, which is the cardinality as a term in `ℕ∞`. We use this function extensively in building the API; it is preferable to both `Set.ncard` and `Finset.card` because it allows infinite sets to be handled without splitting into cases.

### The ground `Set` #

A last place where we make a consequential choice is making the ground set of a matroid a structure field of type `Set α` (where `α` is the type of 'possible matroid elements') rather than just having a type `α` of all the matroid elements. This is because of how common it is to simultaneously consider a number of matroids on different but related ground sets. For example, a matroid `M` on ground set `E` can have its structure 'restricted' to some subset `R ⊆ E` to give a smaller matroid `M ↾ R` with ground set `R`. A statement like `(M ↾ R₁) ↾ R₂ = M ↾ R₂` is mathematically obvious. But if the ground set of a matroid is a type, this doesn't typecheck, and is only true up to canonical isomorphism. Restriction is just the tip of the iceberg here; one can also 'contract' and 'delete' elements and sets of elements in a matroid to give a smaller matroid, and in practice it is common to make statements like `M₁.E = M₂.E ∩ M₃.E` and `((M ⟋ e) ↾ R) ⟋ C = M ⟋ (C ∪ {e}) ↾ R`. Such things are a nightmare to work with unless `=` is actually propositional equality (especially because the relevant coercions are usually between sets and not just elements).

So the solution is that the ground set `M.E` has type `Set α`, and there are elements of type `α` that aren't in the matroid. The tradeoff is that for many statements, one now has to add hypotheses of the form `X ⊆ M.E` to make sure than `X` is actually 'in the matroid', rather than letting a 'type of matroid elements' take care of this invisibly. It still seems that this is worth it. The tactic `aesop_mat` exists specifically to discharge such goals with minimal fuss (using default values). The tactic works fairly well, but has room for improvement.

A related decision is to not have matroids themselves be a typeclass. This would make things be notationally simpler (having `Base` in the presence of `[Matroid α]` rather than `M.Base` for a term `M : Matroid α`) but is again just too awkward when one has multiple matroids on the same type. In fact, in regular written mathematics, it is normal to explicitly indicate which matroid something is happening in, so our notation mirrors common practice.

### Notation #

We use a few nonstandard conventions in theorem names that are related to the above. First, we mirror common informal practice by referring explicitly to the `ground` set rather than the notation `E`. (Writing `ground` everywhere in a proof term would be unwieldy, and writing `E` in theorem names would be unnatural to read.)

Second, because we are typically interested in subsets of the ground set `M.E`, using `Set.compl` is inconvenient, since `Xᶜ ⊆ M.E` is typically false for `X ⊆ M.E`. On the other hand (especially when duals arise), it is common to complement a set `X ⊆ M.E` within the ground set, giving `M.E \ X`. For this reason, we use the term `compl` in theorem names to refer to taking a set difference with respect to the ground set, rather than a complement within a type. The lemma `compl_isBase_dual` is one of the many examples of this.

Finally, in theorem names, matroid predicates that apply to sets (such as `Base`, `Indep`, `IsBasis`) are typically used as suffixes rather than prefixes. For instance, we have `ground_indep_iff_isBase` rather than `indep_ground_iff_isBase`.

## References #

- [J. Oxley, Matroid Theory][oxley2011]
- [H. Bruhn, R. Diestel, M. Kriesell, R. Pendavingh, P. Wollan, Axioms for infinite matroids, Adv. Math 239 (2013), 18-46][bruhnDiestelKriesselPendavinghWollan2013]
- [N. Bowler, S. Geschke, Self-dual uniform matroids on infinite sets, Proc. Amer. Math. Soc. 144 (2016), 459-471][bowlerGeschke2015]

source
def Matroid.ExchangeProperty {α : Type u_1} (P : Set α → Prop) :
Prop

A predicate `P` on sets satisfies the exchange property if, for all `X` and `Y` satisfying `P` and all `a ∈ X \ Y`, there exists `b ∈ Y \ X` so that swapping `a` for `b` in `X` maintains `P`.

Equations

- Matroid.ExchangeProperty P = ∀ (X Y : Set α), P X → P Y → ∀ a ∈ X \ Y, ∃ b ∈ Y \ X, P (insert b (X \ {a}))

Instances For

source
def Matroid.ExistsMaximalSubsetProperty {α : Type u_1} (P : Set α → Prop) (X : Set α) :
Prop

A set `X` has the maximal subset property for a predicate `P` if every subset of `X` satisfying `P` is contained in a maximal subset of `X` satisfying `P`.

Equations

- Matroid.ExistsMaximalSubsetProperty P X = ∀ (I : Set α), P I → I ⊆ X → ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) => P K ∧ K ⊆ X) J

Instances For

source
structure Matroid (α : Type u_1) :
Type u_1

A `Matroid α` is a ground set `E` of type `Set α`, and a nonempty collection of its subsets satisfying the exchange property and the maximal subset property. Each such set is called a `Base` of `M`. An `Indep`endent set is just a set contained in a base, but we include this predicate as a structure field for better definitional properties.

In most cases, using this definition directly is not the best way to construct a matroid, since it requires specifying both the bases and independent sets. If the bases are known, use `Matroid.ofBase` or a variant. If just the independent sets are known, define an `IndepMatroid`, and then use `IndepMatroid.matroid`.

- E : Set α

  `M` has a ground set `E`.

- IsBase : Set α → Prop

  `M` has a predicate `Base` defining its bases.

- Indep : Set α → Prop

  `M` has a predicate `Indep` defining its independent sets.

- indep_iff' ⦃I : Set α⦄ : self.Indep I ↔ ∃ (B : Set α), self.IsBase B ∧ I ⊆ B

  The `Indep`endent sets are those contained in `Base`s.

- exists_isBase : ∃ (B : Set α), self.IsBase B

  There is at least one `Base`.

- isBase_exchange : ExchangeProperty self.IsBase

  For any bases `B`, `B'` and `e ∈ B \ B'`, there is some `f ∈ B' \ B` for which `B-e+f` is a base.

- maximality (X : Set α) : X ⊆ self.E → ExistsMaximalSubsetProperty self.Indep X

  Every independent subset `I` of a set `X` for is contained in a maximal independent subset of `X`.

- subset_ground (B : Set α) : self.IsBase B → B ⊆ self.E

  Every base is contained in the ground set.

Instances For

source
theorem Matroid.ext {α : Type u_1} {x y : Matroid α} (E : x.E = y.E) (IsBase : x.IsBase = y.IsBase) (Indep : x.Indep = y.Indep) :
x = y
source
theorem Matroid.ext_iff {α : Type u_1} {x y : Matroid α} :
x = y ↔ x.E = y.E ∧ x.IsBase = y.IsBase ∧ x.Indep = y.Indep
source
instance Matroid.instNonemptySubtypeSetIsBase {α : Type u_1} (M : Matroid α) :
Nonempty { B : Set α // M.IsBase B }
source
class Matroid.Finite {α : Type u_1} (M : Matroid α) :
Prop

Typeclass for a matroid having finite ground set. Just a wrapper for `M.E.Finite`.

- ground_finite : M.E.Finite

  The ground set is finite

Instances

source
theorem Matroid.finite_iff {α : Type u_1} (M : Matroid α) :
M.Finite ↔ M.E.Finite
source
class Matroid.Nonempty {α : Type u_1} (M : Matroid α) :
Prop

Typeclass for a matroid having nonempty ground set. Just a wrapper for `M.E.Nonempty`.

- ground_nonempty : M.E.Nonempty

  The ground set is nonempty

Instances

source
theorem Matroid.ground_nonempty {α : Type u_1} (M : Matroid α) [M.Nonempty] :
M.E.Nonempty
source
theorem Matroid.ground_nonempty_iff {α : Type u_1} (M : Matroid α) :
M.E.Nonempty ↔ M.Nonempty
source
theorem Matroid.nonempty_type {α : Type u_1} (M : Matroid α) [h : M.Nonempty] :
Nonempty α
source
theorem Matroid.ground_finite {α : Type u_1} (M : Matroid α) [M.Finite] :
M.E.Finite
source
theorem Matroid.set_finite {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α) (hX : X ⊆ M.E := by aesop) :
X.Finite
source
instance Matroid.finite_of_finite {α : Type u_1} [Finite α] {M : Matroid α} :
M.Finite
source
class Matroid.RankFinite {α : Type u_1} (M : Matroid α) :
Prop

A `RankFinite` matroid is one whose bases are finite

- exists_finite_isBase : ∃ (B : Set α), M.IsBase B ∧ B.Finite

  There is a finite base

Instances

source
theorem Matroid.rankFinite_iff {α : Type u_1} (M : Matroid α) :
M.RankFinite ↔ ∃ (B : Set α), M.IsBase B ∧ B.Finite
source
instance Matroid.rankFinite_of_finite {α : Type u_1} (M : Matroid α) [M.Finite] :
M.RankFinite
source
class Matroid.RankInfinite {α : Type u_1} (M : Matroid α) :
Prop

An `RankInfinite` matroid is one whose bases are infinite.

- exists_infinite_isBase : ∃ (B : Set α), M.IsBase B ∧ B.Infinite

  There is an infinite base

Instances

source
theorem Matroid.rankInfinite_iff {α : Type u_1} (M : Matroid α) :
M.RankInfinite ↔ ∃ (B : Set α), M.IsBase B ∧ B.Infinite
source
class Matroid.RankPos {α : Type u_1} (M : Matroid α) :
Prop

A `RankPos` matroid is one whose bases are nonempty.

- empty_not_isBase : ¬M.IsBase ∅

  The empty set isn't a base

Instances

source
theorem Matroid.rankPos_iff {α : Type u_1} (M : Matroid α) :
M.RankPos ↔ ¬M.IsBase ∅
source
instance Matroid.rankPos_nonempty {α : Type u_1} {M : Matroid α} [M.RankPos] :
M.Nonempty
source
theorem Matroid.ExchangeProperty.antichain {α : Type u_1} {IsBase : Set α → Prop} {B B' : Set α} (exch : ExchangeProperty IsBase) (hB : IsBase B) (hB' : IsBase B') (h : B ⊆ B') :
B = B'

A family of sets with the exchange property is an antichain.

source
@[irreducible]
theorem Matroid.ExchangeProperty.encard_diff_le_aux {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α} (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
source
theorem Matroid.ExchangeProperty.encard_diff_eq {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α} (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
(B₁ \ B₂).encard = (B₂ \ B₁).encard

For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂` and `B₂ \ B₁` have the same `ℕ∞`-cardinality.

source
theorem Matroid.ExchangeProperty.encard_isBase_eq {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α} (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
B₁.encard = B₂.encard

Any two sets `B₁`, `B₂` in a family with the exchange property have the same `ℕ∞`-cardinality.

source
def Matroid.aesop_mat :
Lean.ParserDescr

The `aesop_mat` tactic attempts to prove a set is contained in the ground set of a matroid. It uses a `[Matroid]` ruleset, and is allowed to fail.

Equations

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

Instances For

source
theorem Matroid.IsBase.subset_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :
B ⊆ M.E
source
theorem Matroid.IsBase.exchange {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hx : e ∈ B₁ \ B₂) :
∃ y ∈ B₂ \ B₁, M.IsBase (insert y (B₁ \ {e}))
source
theorem Matroid.IsBase.exchange_mem {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hxB₁ : e ∈ B₁) (hxB₂ : e ∉ B₂) :
∃ (y : α), (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))
source
theorem Matroid.IsBase.eq_of_subset_isBase {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hB₁B₂ : B₁ ⊆ B₂) :
B₁ = B₂
source
theorem Matroid.IsBase.not_isBase_of_ssubset {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.IsBase B) (hX : X ⊂ B) :
¬M.IsBase X
source
theorem Matroid.IsBase.insert_not_isBase {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (heB : e ∉ B) :
¬M.IsBase (insert e B)
source
theorem Matroid.IsBase.encard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
(B₁ \ B₂).encard = (B₂ \ B₁).encard
source
theorem Matroid.IsBase.ncard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
(B₁ \ B₂).ncard = (B₂ \ B₁).ncard
source
theorem Matroid.IsBase.encard_eq_encard_of_isBase {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
B₁.encard = B₂.encard
source
theorem Matroid.IsBase.ncard_eq_ncard_of_isBase {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
B₁.ncard = B₂.ncard
source
theorem Matroid.IsBase.finite_of_finite {α : Type u_1} {M : Matroid α} {B B' : Set α} (hB : M.IsBase B) (h : B.Finite) (hB' : M.IsBase B') :
B'.Finite
source
theorem Matroid.IsBase.infinite_of_infinite {α : Type u_1} {M : Matroid α} {B B₁ : Set α} (hB : M.IsBase B) (h : B.Infinite) (hB₁ : M.IsBase B₁) :
B₁.Infinite
source
theorem Matroid.IsBase.finite {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankFinite] (hB : M.IsBase B) :
B.Finite
source
theorem Matroid.IsBase.infinite {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankInfinite] (hB : M.IsBase B) :
B.Infinite
source
theorem Matroid.empty_not_isBase {α : Type u_1} {M : Matroid α} [h : M.RankPos] :
¬M.IsBase ∅
source
theorem Matroid.IsBase.nonempty {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankPos] (hB : M.IsBase B) :
B.Nonempty
source
theorem Matroid.IsBase.rankPos_of_nonempty {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) (h : B.Nonempty) :
M.RankPos
source
theorem Matroid.IsBase.rankFinite_of_finite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) (hfin : B.Finite) :
M.RankFinite
source
theorem Matroid.IsBase.rankInfinite_of_infinite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) (h : B.Infinite) :
M.RankInfinite
source
theorem Matroid.not_rankFinite {α : Type u_1} (M : Matroid α) [M.RankInfinite] :
¬M.RankFinite
source
theorem Matroid.not_rankInfinite {α : Type u_1} (M : Matroid α) [M.RankFinite] :
¬M.RankInfinite
source
theorem Matroid.rankFinite_or_rankInfinite {α : Type u_1} (M : Matroid α) :
M.RankFinite ∨ M.RankInfinite
source
@[simp]
theorem Matroid.not_rankFinite_iff {α : Type u_1} (M : Matroid α) :
¬M.RankFinite ↔ M.RankInfinite
source
@[simp]
theorem Matroid.not_rankInfinite_iff {α : Type u_1} (M : Matroid α) :
¬M.RankInfinite ↔ M.RankFinite
source
theorem Matroid.IsBase.diff_finite_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
(B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite
source
theorem Matroid.IsBase.diff_infinite_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
(B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite
source
theorem Matroid.ext_isBase {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)) :
M₁ = M₂
source
theorem Matroid.ext_iff_isBase {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
source
theorem Matroid.isBase_compl_iff_maximal_disjoint_isBase {α : Type u_1} {M : Matroid α} {B : Set α} (hB : B ⊆ M.E := by aesop_mat) :
M.IsBase (M.E \ B) ↔ Maximal (fun (I : Set α) => I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) B
source
def Matroid.Dep {α : Type u_1} (M : Matroid α) (D : Set α) :
Prop

A subset of `M.E` is `Dep`endent if it is not `Indep`endent .

Equations

- M.Dep D = (¬M.Indep D ∧ D ⊆ M.E)

Instances For

source
theorem Matroid.indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Indep I ↔ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B
source
theorem Matroid.setOf_indep_eq {α : Type u_1} (M : Matroid α) :
{I : Set α | M.Indep I} = ↑(lowerClosure {B : Set α | M.IsBase B})
source
theorem Matroid.Indep.exists_isBase_superset {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
∃ (B : Set α), M.IsBase B ∧ I ⊆ B
source
theorem Matroid.dep_iff {α : Type u_1} {M : Matroid α} {D : Set α} :
M.Dep D ↔ ¬M.Indep D ∧ D ⊆ M.E
source
theorem Matroid.setOf_dep_eq {α : Type u_1} (M : Matroid α) :
{D : Set α | M.Dep D} = {I : Set α | M.Indep I}ᶜ ∩ Set.Iic M.E
source
theorem Matroid.Indep.subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
I ⊆ M.E
source
theorem Matroid.Dep.subset_ground {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
D ⊆ M.E
source
theorem Matroid.indep_or_dep {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
M.Indep X ∨ M.Dep X
source
theorem Matroid.Indep.not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
¬M.Dep I
source
theorem Matroid.Dep.not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
¬M.Indep D
source
theorem Matroid.dep_of_not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : ¬M.Indep D) (hDE : D ⊆ M.E := by aesop_mat) :
M.Dep D
source
theorem Matroid.indep_of_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : ¬M.Dep I) (hIE : I ⊆ M.E := by aesop_mat) :
M.Indep I
source
@[simp]
theorem Matroid.not_dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
¬M.Dep X ↔ M.Indep X
source
@[simp]
theorem Matroid.not_indep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
¬M.Indep X ↔ M.Dep X
source
theorem Matroid.indep_iff_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E
source
theorem Matroid.Indep.subset {α : Type u_1} {M : Matroid α} {I J : Set α} (hJ : M.Indep J) (hIJ : I ⊆ J) :
M.Indep I
source
theorem Matroid.Dep.superset {α : Type u_1} {M : Matroid α} {D X : Set α} (hD : M.Dep D) (hDX : D ⊆ X) (hXE : X ⊆ M.E := by aesop_mat) :
M.Dep X
source
theorem Matroid.IsBase.indep {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :
M.Indep B
source
@[simp]
theorem Matroid.empty_indep {α : Type u_1} (M : Matroid α) :
M.Indep ∅
source
theorem Matroid.Dep.nonempty {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
D.Nonempty
source
theorem Matroid.Indep.finite {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite] (hI : M.Indep I) :
I.Finite
source
theorem Matroid.Indep.rankPos_of_nonempty {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hne : I.Nonempty) :
M.RankPos
source
theorem Matroid.Indep.inter_right {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
M.Indep (I ∩ X)
source
theorem Matroid.Indep.inter_left {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
M.Indep (X ∩ I)
source
theorem Matroid.Indep.diff {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
M.Indep (I \ X)
source
theorem Matroid.IsBase.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {B I : Set α} (hB : M.IsBase B) (hI : M.Indep I) (hBI : B ⊆ I) :
B = I
source
theorem Matroid.isBase_iff_maximal_indep {α : Type u_1} {M : Matroid α} {B : Set α} :
M.IsBase B ↔ Maximal M.Indep B
source
theorem Matroid.Indep.isBase_of_maximal {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J) :
M.IsBase I
source
theorem Matroid.IsBase.dep_of_ssubset {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.IsBase B) (h : B ⊂ X) (hX : X ⊆ M.E := by aesop_mat) :
M.Dep X
source
theorem Matroid.IsBase.dep_of_insert {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (heB : e ∉ B) (he : e ∈ M.E := by aesop_mat) :
M.Dep (insert e B)
source
theorem Matroid.IsBase.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (heB : M.Indep (insert e B)) :
e ∈ B
source
theorem Matroid.IsBase.eq_exchange_of_diff_eq_singleton {α : Type u_1} {M : Matroid α} {B B' : Set α} {e : α} (hB : M.IsBase B) (hB' : M.IsBase B') (h : B \ B' = {e}) :
∃ f ∈ B' \ B, B' = insert f B \ {e}

If the difference of two IsBases is a singleton, then they differ by an insertion/removal

source
theorem Matroid.IsBase.exchange_isBase_of_indep {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : M.IsBase B) (hf : f ∉ B) (hI : M.Indep (insert f (B \ {e}))) :
M.IsBase (insert f (B \ {e}))
source
theorem Matroid.IsBase.exchange_isBase_of_indep' {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : M.IsBase B) (he : e ∈ B) (hf : f ∉ B) (hI : M.Indep (insert f B \ {e})) :
M.IsBase (insert f B \ {e})
source
theorem Matroid.insert_isBase_of_insert_indep {α : Type u_1} {M : Matroid α} {I : Set α} {e f : α} (he : e ∉ I) (hf : f ∉ I) (heI : M.IsBase (insert e I)) (hfI : M.Indep (insert f I)) :
M.IsBase (insert f I)
source
theorem Matroid.IsBase.insert_dep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (h : e ∈ M.E \ B) :
M.Dep (insert e B)
source
theorem Matroid.Indep.exists_insert_of_not_isBase {α : Type u_1} {M : Matroid α} {B I : Set α} (hI : M.Indep I) (hI' : ¬M.IsBase I) (hB : M.IsBase B) :
∃ e ∈ B \ I, M.Indep (insert e I)
source
theorem Matroid.Indep.exists_insert_of_not_maximal {α : Type u_1} (M : Matroid α) ⦃I B : Set α⦄ (hI : M.Indep I) (hInotmax : ¬Maximal M.Indep I) (hB : Maximal M.Indep B) :
∃ x ∈ B \ I, M.Indep (insert x I)

This is the same as `Indep.exists_insert_of_not_isBase`, but phrased so that it is defeq to the augmentation axiom for independent sets.

source
theorem Matroid.Indep.isBase_of_forall_insert {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Indep B) (hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)) :
M.IsBase B
source
theorem Matroid.ground_indep_iff_isBase {α : Type u_1} {M : Matroid α} :
M.Indep M.E ↔ M.IsBase M.E
source
theorem Matroid.IsBase.exists_insert_of_ssubset {α : Type u_1} {M : Matroid α} {B B' I : Set α} (hB : M.IsBase B) (hIB : I ⊂ B) (hB' : M.IsBase B') :
∃ e ∈ B' \ I, M.Indep (insert e I)
source
theorem Matroid.ext_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) :
M₁ = M₂
source
theorem Matroid.ext_indep_iff {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
source
theorem Matroid.ext_iff_indep {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
source
theorem Matroid.ext_isBase_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B) (hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B) :
M₁ = M₂

If every base of `M₁` is independent in `M₂` and vice versa, then `M₁ = M₂`.

source
class Matroid.Finitary {α : Type u_1} (M : Matroid α) :
Prop

A `Finitary` matroid is one where a set is independent if and only if it all its finite subsets are independent, or equivalently a matroid whose circuits are finite.

- indep_of_forall_finite (I : Set α) : (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I

  `I` is independent if all its finite subsets are independent.

Instances

source
theorem Matroid.finitary_iff {α : Type u_1} (M : Matroid α) :
M.Finitary ↔ ∀ (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I
source
theorem Matroid.indep_of_forall_finite_subset_indep {α : Type u_1} {M : Matroid α} [M.Finitary] (I : Set α) (h : ∀ J ⊆ I, J.Finite → M.Indep J) :
M.Indep I
source
theorem Matroid.indep_iff_forall_finite_subset_indep {α : Type u_1} {I : Set α} {M : Matroid α} [M.Finitary] :
M.Indep I ↔ ∀ J ⊆ I, J.Finite → M.Indep J
source
instance Matroid.finitary_of_rankFinite {α : Type u_1} {M : Matroid α} [M.RankFinite] :
M.Finitary
source
theorem Matroid.existsMaximalSubsetProperty_indep {α : Type u_1} (M : Matroid α) (X : Set α) :
X ⊆ M.E → ExistsMaximalSubsetProperty M.Indep X

Matroids obey the maximality axiom

source
def Matroid.copy {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E) (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) :
Matroid α

create a copy of `M : Matroid α` with independence and base predicates and ground set defeq to supplied arguments that are provably equal to those of `M`.

Equations

- M.copy E IsBase Indep hE hB hI = { E := E, IsBase := IsBase, Indep := Indep, indep_iff' := ⋯, exists_isBase := ⋯, isBase_exchange := ⋯, maximality := ⋯, subset_ground := ⋯ }

Instances For

source
@[simp]
theorem Matroid.copy_IsBase {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E) (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) (a✝ : Set α) :
(M.copy E IsBase Indep hE hB hI).IsBase a✝ = IsBase a✝
source
@[simp]
theorem Matroid.copy_E {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E) (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) :
(M.copy E IsBase Indep hE hB hI).E = E
source
@[simp]
theorem Matroid.copy_Indep {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E) (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) (a✝ : Set α) :
(M.copy E IsBase Indep hE hB hI).Indep a✝ = Indep a✝
source
def Matroid.copyIndep {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E) (h : ∀ (I : Set α), Indep I ↔ M.Indep I) :
Matroid α

create a copy of `M : Matroid α` with an independence predicate and ground set defeq to supplied arguments that are provably equal to those of `M`.

Equations

- M.copyIndep E Indep hE h = M.copy E M.IsBase Indep hE ⋯ h

Instances For

source
@[simp]
theorem Matroid.copyIndep_E {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E) (h : ∀ (I : Set α), Indep I ↔ M.Indep I) :
(M.copyIndep E Indep hE h).E = E
source
@[simp]
theorem Matroid.copyIndep_IsBase {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E) (h : ∀ (I : Set α), Indep I ↔ M.Indep I) (a✝ : Set α) :
(M.copyIndep E Indep hE h).IsBase a✝ = M.IsBase a✝
source
@[simp]
theorem Matroid.copyIndep_Indep {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E) (h : ∀ (I : Set α), Indep I ↔ M.Indep I) (a✝ : Set α) :
(M.copyIndep E Indep hE h).Indep a✝ = Indep a✝
source
def Matroid.copyBase {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E) (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) :
Matroid α

create a copy of `M : Matroid α` with a base predicate and ground set defeq to supplied arguments that are provably equal to those of `M`.

Equations

- M.copyBase E IsBase hE h = M.copy E IsBase M.Indep hE h ⋯

Instances For

source
@[simp]
theorem Matroid.copyBase_Indep {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E) (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (a✝ : Set α) :
(M.copyBase E IsBase hE h).Indep a✝ = M.Indep a✝
source
@[simp]
theorem Matroid.copyBase_E {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E) (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) :
(M.copyBase E IsBase hE h).E = E
source
@[simp]
theorem Matroid.copyBase_IsBase {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E) (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (a✝ : Set α) :
(M.copyBase E IsBase hE h).IsBase a✝ = IsBase a✝
source
def Matroid.IsBasis {α : Type u_1} (M : Matroid α) (I X : Set α) :
Prop

A Basis for a set `X ⊆ M.E` is a maximal independent subset of `X` (Often in the literature, the word 'Basis' is used to refer to what we call a 'Base').

Equations

- M.IsBasis I X = (Maximal (fun (A : Set α) => M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E)

Instances For

source
def Matroid.IsBasis' {α : Type u_1} (M : Matroid α) (I X : Set α) :
Prop

`Matroid.IsBasis' I X` is the same as `Matroid.IsBasis I X`, without the requirement that `X ⊆ M.E`. This is convenient for some API building, especially when working with rank and closure.

Equations

- M.IsBasis' I X = Maximal (fun (A : Set α) => M.Indep A ∧ A ⊆ X) I

Instances For

source
theorem Matroid.IsBasis'.indep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) :
M.Indep I
source
theorem Matroid.IsBasis.indep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
M.Indep I
source
theorem Matroid.IsBasis.subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
I ⊆ X
source
theorem Matroid.IsBasis.isBasis' {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
M.IsBasis' I X
source
theorem Matroid.IsBasis'.isBasis {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) (hX : X ⊆ M.E := by aesop_mat) :
M.IsBasis I X
source
theorem Matroid.IsBasis'.subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) :
I ⊆ X
source
theorem Matroid.IsBasis.subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
X ⊆ M.E
source
theorem Matroid.IsBasis.isBasis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
M.IsBasis I (X ∩ M.E)
source
theorem Matroid.IsBasis.left_subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
I ⊆ M.E
source
theorem Matroid.IsBasis.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) :
I = J
source
theorem Matroid.IsBasis.Finite {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) [M.RankFinite] :
I.Finite
source
theorem Matroid.isBasis_iff' {α : Type u_1} {M : Matroid α} {I X : Set α} :
M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
source
theorem Matroid.isBasis_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
source
theorem Matroid.isBasis'_iff_isBasis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} :
M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)
source
theorem Matroid.isBasis'_iff_isBasis {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
M.IsBasis' I X ↔ M.IsBasis I X
source
theorem Matroid.isBasis_iff_isBasis'_subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} :
M.IsBasis I X ↔ M.IsBasis' I X ∧ X ⊆ M.E
source
theorem Matroid.IsBasis'.isBasis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) :
M.IsBasis I (X ∩ M.E)
source
theorem Matroid.IsBasis'.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis' I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) :
I = J
source
theorem Matroid.IsBasis'.insert_not_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.IsBasis' I X) (he : e ∈ X \ I) :
¬M.Indep (insert e I)
source
theorem Matroid.isBasis_iff_maximal {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
M.IsBasis I X ↔ Maximal (fun (I : Set α) => M.Indep I ∧ I ⊆ X) I
source
theorem Matroid.Indep.isBasis_of_maximal_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I) (hX : X ⊆ M.E := by aesop_mat) :
M.IsBasis I X
source
theorem Matroid.IsBasis.isBasis_subset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.IsBasis I X) (hIY : I ⊆ Y) (hYX : Y ⊆ X) :
M.IsBasis I Y
source
@[simp]
theorem Matroid.isBasis_self_iff_indep {α : Type u_1} {M : Matroid α} {I : Set α} :
M.IsBasis I I ↔ M.Indep I
source
theorem Matroid.Indep.isBasis_self {α : Type u_1} {M : Matroid α} {I : Set α} (h : M.Indep I) :
M.IsBasis I I
source
@[simp]
theorem Matroid.isBasis_empty_iff {α : Type u_1} {I : Set α} (M : Matroid α) :
M.IsBasis I ∅ ↔ I = ∅
source
theorem Matroid.IsBasis.dep_of_ssubset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.IsBasis I X) (hIY : I ⊂ Y) (hYX : Y ⊆ X) :
M.Dep Y
source
theorem Matroid.IsBasis.insert_dep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.IsBasis I X) (he : e ∈ X \ I) :
M.Dep (insert e I)
source
theorem Matroid.IsBasis.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.IsBasis I X) (he : e ∈ X) (hIe : M.Indep (insert e I)) :
e ∈ I
source
theorem Matroid.IsBasis'.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.IsBasis' I X) (he : e ∈ X) (hIe : M.Indep (insert e I)) :
e ∈ I
source
theorem Matroid.IsBasis.not_isBasis_of_ssubset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) (hJI : J ⊂ I) :
¬M.IsBasis J X
source
theorem Matroid.Indep.subset_isBasis_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hX : X ⊆ M.E := by aesop_mat) :
∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J
source
theorem Matroid.Indep.subset_isBasis'_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) :
∃ (J : Set α), M.IsBasis' J X ∧ I ⊆ J
source
theorem Matroid.exists_isBasis {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) :
∃ (I : Set α), M.IsBasis I X
source
theorem Matroid.exists_isBasis' {α : Type u_1} (M : Matroid α) (X : Set α) :
∃ (I : Set α), M.IsBasis' I X
source
theorem Matroid.exists_isBasis_subset_isBasis {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) :
∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
source
theorem Matroid.IsBasis.exists_isBasis_inter_eq_of_superset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.IsBasis I X) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) :
∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I
source
theorem Matroid.exists_isBasis_union_inter_isBasis {α : Type u_1} (M : Matroid α) (X Y : Set α) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) :
∃ (I : Set α), M.IsBasis I (X ∪ Y) ∧ M.IsBasis (I ∩ Y) Y
source
theorem Matroid.Indep.eq_of_isBasis {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.IsBasis J I) :
J = I
source
theorem Matroid.IsBasis.exists_isBase {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
∃ (B : Set α), M.IsBase B ∧ I = B ∩ X
source
@[simp]
theorem Matroid.isBasis_ground_iff {α : Type u_1} {M : Matroid α} {B : Set α} :
M.IsBasis B M.E ↔ M.IsBase B
source
theorem Matroid.IsBase.isBasis_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :
M.IsBasis B M.E
source
theorem Matroid.Indep.isBasis_iff_forall_insert_dep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) :
M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
source
theorem Matroid.Indep.isBasis_of_forall_insert {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (he : ∀ e ∈ X \ I, M.Dep (insert e I)) :
M.IsBasis I X
source
theorem Matroid.Indep.isBasis_insert_iff {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) :
M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I
source
theorem Matroid.IsBasis.iUnion_isBasis_iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} (X I : ι → Set α) (hI : ∀ (i : ι), M.IsBasis (I i) (X i)) (h_ind : M.Indep (⋃ (i : ι), I i)) :
M.IsBasis (⋃ (i : ι), I i) (⋃ (i : ι), X i)
source
theorem Matroid.IsBasis.isBasis_iUnion {α : Type u_1} {M : Matroid α} {I : Set α} {ι : Type u_2} [Nonempty ι] (X : ι → Set α) (hI : ∀ (i : ι), M.IsBasis I (X i)) :
M.IsBasis I (⋃ (i : ι), X i)
source
theorem Matroid.IsBasis.isBasis_sUnion {α : Type u_1} {M : Matroid α} {I : Set α} {Xs : Set (Set α)} (hne : Xs.Nonempty) (h : ∀ X ∈ Xs, M.IsBasis I X) :
M.IsBasis I (⋃₀ Xs)
source
theorem Matroid.Indep.isBasis_setOf_insert_isBasis {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
M.IsBasis I {x : α | M.IsBasis I (insert x I)}
source
theorem Matroid.IsBasis.union_isBasis_union {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y) (h : M.Indep (I ∪ J)) :
M.IsBasis (I ∪ J) (X ∪ Y)
source
theorem Matroid.IsBasis.isBasis_union {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hIX : M.IsBasis I X) (hIY : M.IsBasis I Y) :
M.IsBasis I (X ∪ Y)
source
theorem Matroid.IsBasis.isBasis_union_of_subset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) :
M.IsBasis J (J ∪ X)
source
theorem Matroid.IsBasis.insert_isBasis_insert {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.IsBasis I X) (h : M.Indep (insert e I)) :
M.IsBasis (insert e I) (insert e X)
source
theorem Matroid.IsBase.isBase_of_isBasis_superset {α : Type u_1} {M : Matroid α} {B I X : Set α} (hB : M.IsBase B) (hBX : B ⊆ X) (hIX : M.IsBasis I X) :
M.IsBase I
source
theorem Matroid.Indep.exists_isBase_subset_union_isBase {α : Type u_1} {M : Matroid α} {B I : Set α} (hI : M.Indep I) (hB : M.IsBase B) :
∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
source
theorem Matroid.IsBasis.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis I X) (hIJ : I ⊆ J) (hJ : M.Indep J) :
J ∩ X = I
source
theorem Matroid.IsBasis'.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis' I X) (hIJ : I ⊆ J) (hJ : M.Indep J) :
J ∩ X = I
source
theorem Matroid.IsBase.isBasis_of_subset {α : Type u_1} {M : Matroid α} {B X : Set α} (hX : X ⊆ M.E := by aesop_mat) (hB : M.IsBase B) (hBX : B ⊆ X) :
M.IsBasis B X
source
theorem Matroid.exists_isBasis_disjoint_isBasis_of_subset {α : Type u_1} (M : Matroid α) {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) :
∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
source
theorem Matroid.finite_setOf_matroid {α : Type u_1} {E : Set α} (hE : E.Finite) :
{M : Matroid α | M.E ⊆ E}.Finite

For finite `E`, finitely many matroids have ground set contained in `E`.

source
theorem Matroid.finite_setOf_matroid' {α : Type u_1} {E : Set α} (hE : E.Finite) :
{M : Matroid α | M.E = E}.Finite

For finite `E`, finitely many matroids have ground set `E`.