Documentation

Mathlib.Data.Matroid.Basic

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 #

Given M : Matroid α ...

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 [FiniteRk 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. Even though the carrier set is written M.E,

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 couple of 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_base_dual is one of the many examples of this.

References #

[1] The standard text on matroid theory [J. G. Oxley, Matroid Theory, Oxford University Press, New York, 2011.]

[2] The robust axiomatic definition of infinite matroids [H. Bruhn, R. Diestel, M. Kriesell, R. Pendavingh, P. Wollan, Axioms for infinite matroids, Adv. Math 239 (2013), 18-46]

[3] Equicardinality of matroid bases is independent of ZFC. [N. Bowler, S. Geschke, Self-dual uniform matroids on infinite sets, Proc. Amer. Math. Soc. 144 (2016), 459-471]

def Matroid.ExchangeProperty {α : Type u_1} (P : Set α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
Instances For
    def Matroid.ExistsMaximalSubsetProperty {α : Type u_1} (P : Set αProp) (X : Set α) :

    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
    Instances For
      theorem Matroid.ext_iff {α : Type u_1} (x : Matroid α) (y : Matroid α) :
      x = y x.E = y.E x.Base = y.Base x.Indep = y.Indep
      theorem Matroid.ext {α : Type u_1} (x : Matroid α) (y : Matroid α) (E : x.E = y.E) (Base : x.Base = y.Base) (Indep : x.Indep = y.Indep) :
      x = y
      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 Independent 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.

      • Base : Set αProp

        M has a predicate Base definining its bases.

      • Indep : Set αProp

        M has a predicate Indep defining its independent sets.

      • indep_iff' : ∀ ⦃I : Set α⦄, self.Indep I ∃ (B : Set α), self.Base B I B

        The Independent sets are those contained in Bases.

      • exists_base : ∃ (B : Set α), self.Base B

        There is at least one Base.

      • base_exchange : Matroid.ExchangeProperty self.Base

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

      • maximality : Xself.E, Matroid.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.Base BB self.E

        Every base is contained in the ground set.

      Instances For
        theorem Matroid.indep_iff' {α : Type u_1} (self : Matroid α) ⦃I : Set α :
        self.Indep I ∃ (B : Set α), self.Base B I B

        The Independent sets are those contained in Bases.

        theorem Matroid.exists_base {α : Type u_1} (self : Matroid α) :
        ∃ (B : Set α), self.Base B

        There is at least one Base.

        theorem Matroid.base_exchange {α : Type u_1} (self : Matroid α) :

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

        theorem Matroid.maximality {α : Type u_1} (self : Matroid α) (X : Set α) :
        X self.EMatroid.ExistsMaximalSubsetProperty self.Indep X

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

        theorem Matroid.subset_ground {α : Type u_1} (self : Matroid α) (B : Set α) :
        self.Base BB self.E

        Every base is contained in the ground set.

        class Matroid.Finite {α : Type u_1} (M : Matroid α) :

        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
          theorem Matroid.Finite.ground_finite {α : Type u_1} {M : Matroid α} [self : M.Finite] :
          M.E.Finite

          The ground set is finite

          class Matroid.Nonempty {α : Type u_1} (M : Matroid α) :

          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
            theorem Matroid.Nonempty.ground_nonempty {α : Type u_1} {M : Matroid α} [self : M.Nonempty] :
            M.E.Nonempty

            The ground set is nonempty

            theorem Matroid.ground_nonempty {α : Type u_1} (M : Matroid α) [M.Nonempty] :
            M.E.Nonempty
            theorem Matroid.ground_nonempty_iff {α : Type u_1} (M : Matroid α) :
            M.E.Nonempty M.Nonempty
            theorem Matroid.ground_finite {α : Type u_1} (M : Matroid α) [M.Finite] :
            M.E.Finite
            theorem Matroid.set_finite {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α) (hX : autoParam (X M.E) _auto✝) :
            X.Finite
            instance Matroid.finite_of_finite {α : Type u_1} [Finite α] {M : Matroid α} :
            M.Finite
            Equations
            • =
            class Matroid.FiniteRk {α : Type u_1} (M : Matroid α) :

            A FiniteRk matroid is one whose bases are finite

            • exists_finite_base : ∃ (B : Set α), M.Base B B.Finite

              There is a finite base

            Instances
              theorem Matroid.FiniteRk.exists_finite_base {α : Type u_1} {M : Matroid α} [self : M.FiniteRk] :
              ∃ (B : Set α), M.Base B B.Finite

              There is a finite base

              instance Matroid.finiteRk_of_finite {α : Type u_1} (M : Matroid α) [M.Finite] :
              M.FiniteRk
              Equations
              • =
              class Matroid.InfiniteRk {α : Type u_1} (M : Matroid α) :

              An InfiniteRk matroid is one whose bases are infinite.

              • exists_infinite_base : ∃ (B : Set α), M.Base B B.Infinite

                There is an infinite base

              Instances
                theorem Matroid.InfiniteRk.exists_infinite_base {α : Type u_1} {M : Matroid α} [self : M.InfiniteRk] :
                ∃ (B : Set α), M.Base B B.Infinite

                There is an infinite base

                class Matroid.RkPos {α : Type u_1} (M : Matroid α) :

                A RkPos matroid is one whose bases are nonempty.

                • empty_not_base : ¬M.Base

                  The empty set isn't a base

                Instances
                  theorem Matroid.RkPos.empty_not_base {α : Type u_1} {M : Matroid α} [self : M.RkPos] :
                  ¬M.Base

                  The empty set isn't a base

                  theorem Matroid.rkPos_iff_empty_not_base {α : Type u_1} {M : Matroid α} :
                  M.RkPos ¬M.Base
                  theorem Matroid.ExchangeProperty.antichain {α : Type u_1} {Base : Set αProp} (exch : Matroid.ExchangeProperty Base) {B : Set α} {B' : Set α} (hB : Base B) (hB' : Base B') (h : B B') :
                  B = B'

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

                  @[irreducible]
                  theorem Matroid.ExchangeProperty.encard_diff_le_aux {α : Type u_1} {Base : Set αProp} {B₁ : Set α} {B₂ : Set α} (exch : Matroid.ExchangeProperty Base) (hB₁ : Base B₁) (hB₂ : Base B₂) :
                  (B₁ \ B₂).encard (B₂ \ B₁).encard
                  theorem Matroid.ExchangeProperty.encard_diff_eq {α : Type u_1} {Base : Set αProp} (exch : Matroid.ExchangeProperty Base) {B₁ : Set α} {B₂ : Set α} (hB₁ : Base B₁) (hB₂ : Base 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.

                  theorem Matroid.ExchangeProperty.encard_base_eq {α : Type u_1} {Base : Set αProp} (exch : Matroid.ExchangeProperty Base) {B₁ : Set α} {B₂ : Set α} (hB₁ : Base B₁) (hB₂ : Base B₂) :
                  B₁.encard = B₂.encard

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

                  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
                    theorem Matroid.Base.subset_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) :
                    B M.E
                    theorem Matroid.Base.exchange {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} {e : α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hx : e B₁ \ B₂) :
                    yB₂ \ B₁, M.Base (insert y (B₁ \ {e}))
                    theorem Matroid.Base.exchange_mem {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} {e : α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hxB₁ : e B₁) (hxB₂ : eB₂) :
                    ∃ (y : α), (y B₂ yB₁) M.Base (insert y (B₁ \ {e}))
                    theorem Matroid.Base.eq_of_subset_base {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hB₁B₂ : B₁ B₂) :
                    B₁ = B₂
                    theorem Matroid.Base.not_base_of_ssubset {α : Type u_1} {M : Matroid α} {B : Set α} {X : Set α} (hB : M.Base B) (hX : X B) :
                    ¬M.Base X
                    theorem Matroid.Base.insert_not_base {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : eB) :
                    ¬M.Base (insert e B)
                    theorem Matroid.Base.encard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    (B₁ \ B₂).encard = (B₂ \ B₁).encard
                    theorem Matroid.Base.ncard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
                    theorem Matroid.Base.card_eq_card_of_base {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    B₁.encard = B₂.encard
                    theorem Matroid.Base.ncard_eq_ncard_of_base {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    B₁.ncard = B₂.ncard
                    theorem Matroid.Base.finite_of_finite {α : Type u_1} {M : Matroid α} {B : Set α} {B' : Set α} (hB : M.Base B) (h : B.Finite) (hB' : M.Base B') :
                    B'.Finite
                    theorem Matroid.Base.infinite_of_infinite {α : Type u_1} {M : Matroid α} {B : Set α} {B₁ : Set α} (hB : M.Base B) (h : B.Infinite) (hB₁ : M.Base B₁) :
                    B₁.Infinite
                    theorem Matroid.Base.finite {α : Type u_1} {M : Matroid α} {B : Set α} [M.FiniteRk] (hB : M.Base B) :
                    B.Finite
                    theorem Matroid.Base.infinite {α : Type u_1} {M : Matroid α} {B : Set α} [M.InfiniteRk] (hB : M.Base B) :
                    B.Infinite
                    theorem Matroid.empty_not_base {α : Type u_1} {M : Matroid α} [h : M.RkPos] :
                    ¬M.Base
                    theorem Matroid.Base.nonempty {α : Type u_1} {M : Matroid α} {B : Set α} [M.RkPos] (hB : M.Base B) :
                    B.Nonempty
                    theorem Matroid.Base.rkPos_of_nonempty {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (h : B.Nonempty) :
                    M.RkPos
                    theorem Matroid.Base.finiteRk_of_finite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (hfin : B.Finite) :
                    M.FiniteRk
                    theorem Matroid.Base.infiniteRk_of_infinite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (h : B.Infinite) :
                    M.InfiniteRk
                    theorem Matroid.not_finiteRk {α : Type u_1} (M : Matroid α) [M.InfiniteRk] :
                    ¬M.FiniteRk
                    theorem Matroid.not_infiniteRk {α : Type u_1} (M : Matroid α) [M.FiniteRk] :
                    ¬M.InfiniteRk
                    theorem Matroid.finite_or_infiniteRk {α : Type u_1} (M : Matroid α) :
                    M.FiniteRk M.InfiniteRk
                    theorem Matroid.Base.diff_finite_comm {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    (B₁ \ B₂).Finite (B₂ \ B₁).Finite
                    theorem Matroid.Base.diff_infinite_comm {α : Type u_1} {M : Matroid α} {B₁ : Set α} {B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
                    (B₁ \ B₂).Infinite (B₂ \ B₁).Infinite
                    theorem Matroid.eq_of_base_iff_base_forall {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃B : Set α⦄, B M₁.E(M₁.Base B M₂.Base B)) :
                    M₁ = M₂
                    theorem Matroid.base_compl_iff_mem_maximals_disjoint_base {α : Type u_1} {M : Matroid α} {B : Set α} (hB : autoParam (B M.E) _auto✝) :
                    M.Base (M.E \ B) B maximals (fun (x x_1 : Set α) => x x_1) {I : Set α | I M.E ∃ (B : Set α), M.Base B Disjoint I B}
                    def Matroid.Dep {α : Type u_1} (M : Matroid α) (D : Set α) :

                    A subset of M.E is Dependent if it is not Independent .

                    Equations
                    Instances For
                      theorem Matroid.indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
                      M.Indep I ∃ (B : Set α), M.Base B I B
                      theorem Matroid.setOf_indep_eq {α : Type u_1} (M : Matroid α) :
                      {I : Set α | M.Indep I} = (lowerClosure {B : Set α | M.Base B})
                      theorem Matroid.Indep.exists_base_superset {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
                      ∃ (B : Set α), M.Base B I B
                      theorem Matroid.dep_iff {α : Type u_1} {M : Matroid α} {D : Set α} :
                      M.Dep D ¬M.Indep D D M.E
                      theorem Matroid.setOf_dep_eq {α : Type u_1} (M : Matroid α) :
                      {D : Set α | M.Dep D} = {I : Set α | M.Indep I} Set.Iic M.E
                      theorem Matroid.Indep.subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
                      I M.E
                      theorem Matroid.Dep.subset_ground {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
                      D M.E
                      theorem Matroid.indep_or_dep {α : Type u_1} {M : Matroid α} {X : Set α} (hX : autoParam (X M.E) _auto✝) :
                      M.Indep X M.Dep X
                      theorem Matroid.Indep.not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
                      ¬M.Dep I
                      theorem Matroid.Dep.not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
                      ¬M.Indep D
                      theorem Matroid.dep_of_not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : ¬M.Indep D) (hDE : autoParam (D M.E) _auto✝) :
                      M.Dep D
                      theorem Matroid.indep_of_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : ¬M.Dep I) (hIE : autoParam (I M.E) _auto✝) :
                      M.Indep I
                      @[simp]
                      theorem Matroid.not_dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : autoParam (X M.E) _auto✝) :
                      ¬M.Dep X M.Indep X
                      @[simp]
                      theorem Matroid.not_indep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : autoParam (X M.E) _auto✝) :
                      ¬M.Indep X M.Dep X
                      theorem Matroid.indep_iff_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} :
                      M.Indep I ¬M.Dep I I M.E
                      theorem Matroid.Indep.subset {α : Type u_1} {M : Matroid α} {J : Set α} {I : Set α} (hJ : M.Indep J) (hIJ : I J) :
                      M.Indep I
                      theorem Matroid.Dep.superset {α : Type u_1} {M : Matroid α} {D : Set α} {X : Set α} (hD : M.Dep D) (hDX : D X) (hXE : autoParam (X M.E) _auto✝) :
                      M.Dep X
                      theorem Matroid.Base.indep {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) :
                      M.Indep B
                      @[simp]
                      theorem Matroid.empty_indep {α : Type u_1} (M : Matroid α) :
                      M.Indep
                      theorem Matroid.Dep.nonempty {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) :
                      D.Nonempty
                      theorem Matroid.Indep.finite {α : Type u_1} {M : Matroid α} {I : Set α} [M.FiniteRk] (hI : M.Indep I) :
                      I.Finite
                      theorem Matroid.Indep.rkPos_of_nonempty {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hne : I.Nonempty) :
                      M.RkPos
                      theorem Matroid.Indep.inter_right {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
                      M.Indep (I X)
                      theorem Matroid.Indep.inter_left {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
                      M.Indep (X I)
                      theorem Matroid.Indep.diff {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) :
                      M.Indep (I \ X)
                      theorem Matroid.Base.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {B : Set α} {I : Set α} (hB : M.Base B) (hI : M.Indep I) (hBI : B I) :
                      B = I
                      theorem Matroid.base_iff_maximal_indep {α : Type u_1} {M : Matroid α} {B : Set α} :
                      M.Base B M.Indep B ∀ (I : Set α), M.Indep IB IB = I
                      theorem Matroid.setOf_base_eq_maximals_setOf_indep {α : Type u_1} {M : Matroid α} :
                      {B : Set α | M.Base B} = maximals (fun (x x_1 : Set α) => x x_1) {I : Set α | M.Indep I}
                      theorem Matroid.Indep.base_of_maximal {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : ∀ (J : Set α), M.Indep JI JI = J) :
                      M.Base I
                      theorem Matroid.Base.dep_of_ssubset {α : Type u_1} {M : Matroid α} {B : Set α} {X : Set α} (hB : M.Base B) (h : B X) (hX : autoParam (X M.E) _auto✝) :
                      M.Dep X
                      theorem Matroid.Base.dep_of_insert {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : eB) (he : autoParam (e M.E) _auto✝) :
                      M.Dep (insert e B)
                      theorem Matroid.Base.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : M.Indep (insert e B)) :
                      e B
                      theorem Matroid.Base.eq_exchange_of_diff_eq_singleton {α : Type u_1} {M : Matroid α} {B : Set α} {B' : Set α} {e : α} (hB : M.Base B) (hB' : M.Base B') (h : B \ B' = {e}) :
                      fB' \ B, B' = insert f B \ {e}

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

                      theorem Matroid.Base.exchange_base_of_indep {α : Type u_1} {M : Matroid α} {B : Set α} {f : α} {e : α} (hB : M.Base B) (hf : fB) (hI : M.Indep (insert f (B \ {e}))) :
                      M.Base (insert f (B \ {e}))
                      theorem Matroid.Base.exchange_base_of_indep' {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} {f : α} (hB : M.Base B) (he : e B) (hf : fB) (hI : M.Indep (insert f B \ {e})) :
                      M.Base (insert f B \ {e})
                      theorem Matroid.Base.insert_dep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (h : e M.E \ B) :
                      M.Dep (insert e B)
                      theorem Matroid.Indep.exists_insert_of_not_base {α : Type u_1} {M : Matroid α} {I : Set α} {B : Set α} (hI : M.Indep I) (hI' : ¬M.Base I) (hB : M.Base B) :
                      eB \ I, M.Indep (insert e I)
                      theorem Matroid.Indep.exists_insert_of_not_mem_maximals {α : Type u_1} (M : Matroid α) ⦃I : Set α ⦃B : Set α (hI : M.Indep I) (hInotmax : Imaximals (fun (x x_1 : Set α) => x x_1) {I : Set α | M.Indep I}) (hB : B maximals (fun (x x_1 : Set α) => x x_1) {I : Set α | M.Indep I}) :
                      xB \ I, M.Indep (insert x I)

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

                      theorem Matroid.ground_indep_iff_base {α : Type u_1} {M : Matroid α} :
                      M.Indep M.E M.Base M.E
                      theorem Matroid.Base.exists_insert_of_ssubset {α : Type u_1} {M : Matroid α} {B : Set α} {I : Set α} {B' : Set α} (hB : M.Base B) (hIB : I B) (hB' : M.Base B') :
                      eB' \ I, M.Indep (insert e I)
                      theorem Matroid.eq_of_indep_iff_indep_forall {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : IM₁.E, M₁.Indep I M₂.Indep I) :
                      M₁ = M₂
                      theorem Matroid.eq_iff_indep_iff_indep_forall {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} :
                      M₁ = M₂ M₁.E = M₂.E IM₁.E, M₁.Indep I M₂.Indep I
                      class Matroid.Finitary {α : Type u_1} (M : Matroid α) :

                      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 α), (JI, J.FiniteM.Indep J)M.Indep I

                        I is independent if all its finite subsets are independent.

                      Instances
                        theorem Matroid.Finitary.indep_of_forall_finite {α : Type u_1} {M : Matroid α} [self : M.Finitary] (I : Set α) :
                        (JI, J.FiniteM.Indep J)M.Indep I

                        I is independent if all its finite subsets are independent.

                        theorem Matroid.indep_of_forall_finite_subset_indep {α : Type u_1} {M : Matroid α} [M.Finitary] (I : Set α) (h : JI, J.FiniteM.Indep J) :
                        M.Indep I
                        theorem Matroid.indep_iff_forall_finite_subset_indep {α : Type u_1} {I : Set α} {M : Matroid α} [M.Finitary] :
                        M.Indep I JI, J.FiniteM.Indep J
                        instance Matroid.finitary_of_finiteRk {α : Type u_1} {M : Matroid α} [M.FiniteRk] :
                        M.Finitary
                        Equations
                        • =
                        theorem Matroid.existsMaximalSubsetProperty_indep {α : Type u_1} (M : Matroid α) (X : Set α) :

                        Matroids obey the maximality axiom

                        def Matroid.Basis {α : Type u_1} (M : Matroid α) (I : Set α) (X : Set α) :

                        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
                        Instances For
                          def Matroid.Basis' {α : Type u_1} (M : Matroid α) (I : Set α) (X : Set α) :

                          A Basis' is a basis without the requirement that X ⊆ M.E. This is convenient for some API building, especially when working with rank and closure.

                          Equations
                          Instances For
                            theorem Matroid.Basis'.indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis' I X) :
                            M.Indep I
                            theorem Matroid.Basis.indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            M.Indep I
                            theorem Matroid.Basis.subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            I X
                            theorem Matroid.Basis.basis' {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            M.Basis' I X
                            theorem Matroid.Basis'.basis {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis' I X) (hX : autoParam (X M.E) _auto✝) :
                            M.Basis I X
                            theorem Matroid.Basis'.subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis' I X) :
                            I X
                            theorem Matroid.setOf_basis_eq {α : Type u_1} {X : Set α} (M : Matroid α) (hX : autoParam (X M.E) _auto✝) :
                            {I : Set α | M.Basis I X} = maximals (fun (x x_1 : Set α) => x x_1) ({I : Set α | M.Indep I} Set.Iic X)
                            theorem Matroid.Basis.subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            X M.E
                            theorem Matroid.Basis.basis_inter_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            M.Basis I (X M.E)
                            theorem Matroid.Basis.left_subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            I M.E
                            theorem Matroid.Basis.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hI : M.Basis I X) (hJ : M.Indep J) (hIJ : I J) (hJX : J X) :
                            I = J
                            theorem Matroid.Basis.Finite {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) [M.FiniteRk] :
                            I.Finite
                            theorem Matroid.basis_iff' {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} :
                            M.Basis I X (M.Indep I I X ∀ (J : Set α), M.Indep JI JJ XI = J) X M.E
                            theorem Matroid.basis_iff {α : Type u_1} {M : Matroid α} {X : Set α} {I : Set α} (hX : autoParam (X M.E) _auto✝) :
                            M.Basis I X M.Indep I I X ∀ (J : Set α), M.Indep JI JJ XI = J
                            theorem Matroid.basis'_iff_basis_inter_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} :
                            M.Basis' I X M.Basis I (X M.E)
                            theorem Matroid.basis'_iff_basis {α : Type u_1} {M : Matroid α} {X : Set α} {I : Set α} (hX : autoParam (X M.E) _auto✝) :
                            M.Basis' I X M.Basis I X
                            theorem Matroid.basis_iff_basis'_subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} :
                            M.Basis I X M.Basis' I X X M.E
                            theorem Matroid.Basis'.basis_inter_ground {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hIX : M.Basis' I X) :
                            M.Basis I (X M.E)
                            theorem Matroid.Basis'.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hI : M.Basis' I X) (hJ : M.Indep J) (hIJ : I J) (hJX : J X) :
                            I = J
                            theorem Matroid.Basis'.insert_not_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {e : α} (hI : M.Basis' I X) (he : e X \ I) :
                            ¬M.Indep (insert e I)
                            theorem Matroid.basis_iff_mem_maximals {α : Type u_1} {M : Matroid α} {X : Set α} {I : Set α} (hX : autoParam (X M.E) _auto✝) :
                            M.Basis I X I maximals (fun (x x_1 : Set α) => x x_1) {I : Set α | M.Indep I I X}
                            theorem Matroid.basis_iff_mem_maximals_Prop {α : Type u_1} {M : Matroid α} {X : Set α} {I : Set α} (hX : autoParam (X M.E) _auto✝) :
                            M.Basis I X I maximals (fun (x x_1 : Set α) => x x_1) fun (I : Set α) => M.Indep I I X
                            theorem Matroid.Indep.basis_of_maximal_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Indep I) (hIX : I X) (hmax : ∀ ⦃J : Set α⦄, M.Indep JI JJ XJ I) (hX : autoParam (X M.E) _auto✝) :
                            M.Basis I X
                            theorem Matroid.Basis.basis_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {Y : Set α} (hI : M.Basis I X) (hIY : I Y) (hYX : Y X) :
                            M.Basis I Y
                            @[simp]
                            theorem Matroid.basis_self_iff_indep {α : Type u_1} {M : Matroid α} {I : Set α} :
                            M.Basis I I M.Indep I
                            theorem Matroid.Indep.basis_self {α : Type u_1} {M : Matroid α} {I : Set α} (h : M.Indep I) :
                            M.Basis I I
                            @[simp]
                            theorem Matroid.basis_empty_iff {α : Type u_1} {I : Set α} (M : Matroid α) :
                            M.Basis I I =
                            theorem Matroid.Basis.dep_of_ssubset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {Y : Set α} (hI : M.Basis I X) (hIY : I Y) (hYX : Y X) :
                            M.Dep Y
                            theorem Matroid.Basis.insert_dep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {e : α} (hI : M.Basis I X) (he : e X \ I) :
                            M.Dep (insert e I)
                            theorem Matroid.Basis.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {e : α} (hI : M.Basis I X) (he : e X) (hIe : M.Indep (insert e I)) :
                            e I
                            theorem Matroid.Basis'.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {e : α} (hI : M.Basis' I X) (he : e X) (hIe : M.Indep (insert e I)) :
                            e I
                            theorem Matroid.Basis.not_basis_of_ssubset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hI : M.Basis I X) (hJI : J I) :
                            ¬M.Basis J X
                            theorem Matroid.Indep.subset_basis_of_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Indep I) (hIX : I X) (hX : autoParam (X M.E) _auto✝) :
                            ∃ (J : Set α), M.Basis J X I J
                            theorem Matroid.Indep.subset_basis'_of_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Indep I) (hIX : I X) :
                            ∃ (J : Set α), M.Basis' J X I J
                            theorem Matroid.exists_basis {α : Type u_1} (M : Matroid α) (X : Set α) (hX : autoParam (X M.E) _auto✝) :
                            ∃ (I : Set α), M.Basis I X
                            theorem Matroid.exists_basis' {α : Type u_1} (M : Matroid α) (X : Set α) :
                            ∃ (I : Set α), M.Basis' I X
                            theorem Matroid.exists_basis_subset_basis {α : Type u_1} {X : Set α} {Y : Set α} (M : Matroid α) (hXY : X Y) (hY : autoParam (Y M.E) _auto✝) :
                            ∃ (I : Set α) (J : Set α), M.Basis I X M.Basis J Y I J
                            theorem Matroid.Basis.exists_basis_inter_eq_of_superset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {Y : Set α} (hI : M.Basis I X) (hXY : X Y) (hY : autoParam (Y M.E) _auto✝) :
                            ∃ (J : Set α), M.Basis J Y J X = I
                            theorem Matroid.exists_basis_union_inter_basis {α : Type u_1} (M : Matroid α) (X : Set α) (Y : Set α) (hX : autoParam (X M.E) _auto✝) (hY : autoParam (Y M.E) _auto✝) :
                            ∃ (I : Set α), M.Basis I (X Y) M.Basis (I Y) Y
                            theorem Matroid.Indep.eq_of_basis {α : Type u_1} {M : Matroid α} {I : Set α} {J : Set α} (hI : M.Indep I) (hJ : M.Basis J I) :
                            J = I
                            theorem Matroid.Basis.exists_base {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Basis I X) :
                            ∃ (B : Set α), M.Base B I = B X
                            @[simp]
                            theorem Matroid.basis_ground_iff {α : Type u_1} {M : Matroid α} {B : Set α} :
                            M.Basis B M.E M.Base B
                            theorem Matroid.Base.basis_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) :
                            M.Basis B M.E
                            theorem Matroid.Indep.basis_iff_forall_insert_dep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Indep I) (hIX : I X) :
                            M.Basis I X eX \ I, M.Dep (insert e I)
                            theorem Matroid.Indep.basis_of_forall_insert {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} (hI : M.Indep I) (hIX : I X) (he : eX \ I, M.Dep (insert e I)) :
                            M.Basis I X
                            theorem Matroid.Indep.basis_insert_iff {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) :
                            M.Basis I (insert e I) M.Dep (insert e I) e I
                            theorem Matroid.Basis.iUnion_basis_iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} (X : ιSet α) (I : ιSet α) (hI : ∀ (i : ι), M.Basis (I i) (X i)) (h_ind : M.Indep (⋃ (i : ι), I i)) :
                            M.Basis (⋃ (i : ι), I i) (⋃ (i : ι), X i)
                            theorem Matroid.Basis.basis_iUnion {α : Type u_1} {M : Matroid α} {I : Set α} {ι : Type u_2} [Nonempty ι] (X : ιSet α) (hI : ∀ (i : ι), M.Basis I (X i)) :
                            M.Basis I (⋃ (i : ι), X i)
                            theorem Matroid.Basis.basis_sUnion {α : Type u_1} {M : Matroid α} {I : Set α} {Xs : Set (Set α)} (hne : Xs.Nonempty) (h : XXs, M.Basis I X) :
                            M.Basis I (⋃₀ Xs)
                            theorem Matroid.Indep.basis_setOf_insert_basis {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
                            M.Basis I {x : α | M.Basis I (insert x I)}
                            theorem Matroid.Basis.union_basis_union {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} {Y : Set α} (hIX : M.Basis I X) (hJY : M.Basis J Y) (h : M.Indep (I J)) :
                            M.Basis (I J) (X Y)
                            theorem Matroid.Basis.basis_union {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {Y : Set α} (hIX : M.Basis I X) (hIY : M.Basis I Y) :
                            M.Basis I (X Y)
                            theorem Matroid.Basis.basis_union_of_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hI : M.Basis I X) (hJ : M.Indep J) (hIJ : I J) :
                            M.Basis J (J X)
                            theorem Matroid.Basis.insert_basis_insert {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {e : α} (hI : M.Basis I X) (h : M.Indep (insert e I)) :
                            M.Basis (insert e I) (insert e X)
                            theorem Matroid.Base.base_of_basis_superset {α : Type u_1} {M : Matroid α} {B : Set α} {X : Set α} {I : Set α} (hB : M.Base B) (hBX : B X) (hIX : M.Basis I X) :
                            M.Base I
                            theorem Matroid.Indep.exists_base_subset_union_base {α : Type u_1} {M : Matroid α} {I : Set α} {B : Set α} (hI : M.Indep I) (hB : M.Base B) :
                            ∃ (B' : Set α), M.Base B' I B' B' I B
                            theorem Matroid.Basis.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hIX : M.Basis I X) (hIJ : I J) (hJ : M.Indep J) :
                            J X = I
                            theorem Matroid.Basis'.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} (hI : M.Basis' I X) (hIJ : I J) (hJ : M.Indep J) :
                            J X = I
                            theorem Matroid.Base.basis_of_subset {α : Type u_1} {M : Matroid α} {X : Set α} {B : Set α} (hX : autoParam (X M.E) _auto✝) (hB : M.Base B) (hBX : B X) :
                            M.Basis B X
                            theorem Matroid.exists_basis_disjoint_basis_of_subset {α : Type u_1} (M : Matroid α) {X : Set α} {Y : Set α} (hXY : X Y) (hY : autoParam (Y M.E) _auto✝) :
                            ∃ (I : Set α) (J : Set α), M.Basis I X M.Basis (I J) Y Disjoint X J
                            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.

                            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.