Matroid Independence and Basis axioms

Matroids in mathlib are defined axiomatically in terms of bases, but can be described just as naturally via their collections of independent sets, and in fact such a description, being more 'verbose', can often be useful. As well as this, the definition of a Matroid uses an unwieldy 'maximality' axiom that can be dropped in cases where there is some finiteness assumption.

This file provides several ways to do define a matroid in terms of its independence or base predicates, using axiom sets that are appropriate in different settings, and often much simpler than the general definition. It also contains simp lemmas and typeclasses as appropriate.

All the independence axiom sets need nontriviality (the empty set is independent), monotonicity (subsets of independent sets are independent), and some form of 'augmentation' axiom, which allows one to enlarge a non-maximal independent set. This augmentation axiom is still required when there are finiteness assumptions, but is simpler. It just states that if I is a finite independent set and J is a larger finite independent set, then there exists e ∈ J \ I for which insert e I is independent. This is the axiom that appears in most of the definitions.

Implementation Details

To facilitate building a matroid from its independent sets, we define a structure IndepMatroid which has a ground set E, an independence predicate Indep, and some axioms as its fields. This structure is another encoding of the data in a Matroid; the function IndepMatroid.matroid constructs a Matroid from an IndepMatroid.

This is convenient because if one wants to define M : Matroid α from a known independence predicate Ind, it is easier to define an M' : IndepMatroid α so that M'.Indep = Ind and then set M = M'.matroid than it is to directly define M with the base axioms. The simp lemma IndepMatroid.matroid_indep_iff is important here; it shows that M.Indep = Ind, so the Matroid constructed is the right one, and the intermediate IndepMatroid can be made essentially invisible by the simplifier when working with M.

Because of this setup, we don't define any API for IndepMatroid, as it would be a redundant copy of the existing API for Matroid.Indep. (In particular, one could define a natural equivalence e : IndepMatroid α ≃ Matroid α with e.toFun = IndepMatroid.matroid, but this would be pointless, as there is no need for the inverse of e).

Main definitions

• IndepMatroid α is a matroid structure on α described in terms of its independent sets in full generality, using infinite versions of the axioms.

• IndepMatroid.matroid turns M' : IndepMatroid α into M : Matroid α with M'.Indep = M.Indep.

• IndepMatroid.ofFinitary constructs an IndepMatroid whose associated Matroid is Finitary in the special case where independence of a set is determined only by that of its finite subsets. This construction uses Zorn's lemma.

• IndepMatroid.ofFinitaryCardAugment is a variant of IndepMatroid.ofFinitary where the augmentation axiom resembles the finite augmentation axiom.

• IndepMatroid.ofBdd constructs an IndepMatroid in the case where there is some known absolute upper bound on the size of an independent set. This uses the infinite version of the augmentation axiom; the corresponding Matroid is RankFinite.

• IndepMatroid.ofBddAugment is the same as the above, but with a finite augmentation axiom.

• IndepMatroid.ofFinite constructs an IndepMatroid from a finite ground set in terms of its independent sets.

• IndepMatroid.ofFinset constructs an IndepMatroid α whose corresponding matroid is Finitary from an independence predicate on Finset α.

• Matroid.ofExistsMatroid constructs a 'copy' of a matroid that is known only existentially, but whose independence predicate is known explicitly.

• Matroid.ofExistsFiniteIsBase constructs a matroid from its bases, if it is known that one of them is finite. This gives a RankFinite matroid.

• Matroid.ofIsBaseOfFinite constructs a Finite matroid from its bases.

structure IndepMatroid (α : Type u_2) : Type u_2

A matroid as defined by a ground set and an independence predicate. This definition is an implementation detail whose purpose is to organize the multiple different versions of the independence axioms; usually, terms of type IndepMatroid should either be directly piped into IndepMatroid.matroid, or should be constructed as a private definition which is then converted into a matroid via IndepMatroid.matroid.

To define a Matroid α from a known independence predicate MyIndep : Set α → Prop and ground set E : Set α, one can either write

def myMatroid (…) : Matroid α :=
  IndepMatroid.matroid <| IndepMatroid.ofFoo E MyIndep _ _ … _

or, slightly more indirectly,

private def myIndepMatroid (…) : IndepMatroid α := IndepMatroid.ofFoo E MyIndep _ _ … _

def myMatroid (…) : Matroid α := (myIndepMatroid …).matroid

In both cases, IndepMatroid.ofFoo is either IndepMatroid.mk, or one of the several other available constructors for IndepMatroid, and the _ represent the proofs that this constructor requires.

After such a definition is made, the facts that myMatroid.Indep = myIndep and myMatroid.E = E are true by either rfl or simp [myMatroid], and can be made directly into @[simp] lemmas.

• E : Set α

  The ground set

• Indep : Set α → Prop

  The independence predicate

• indep_empty : self.Indep ∅
• indep_subset ⦃I J : Set α⦄ : self.Indep J → I ⊆ J → self.Indep I
• indep_aug ⦃I B : Set α⦄ : self.Indep I → ¬Maximal self.Indep I → Maximal self.Indep B → ∃ x ∈ B \ I, self.Indep (insert x I)
• indep_maximal (X : Set α) : X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty self.Indep X
• subset_ground (I : Set α) : self.Indep I → I ⊆ self.E

def IndepMatroid.matroid {α : Type u_1} (M : IndepMatroid α) : Matroid α

An M : IndepMatroid α gives a Matroid α whose bases are the maximal M-independent sets.

Equations

• M.matroid = { E := M.E, IsBase := Maximal M.Indep, Indep := M.Indep, indep_iff' := ⋯, exists_isBase := ⋯, isBase_exchange := ⋯, maximality := ⋯, subset_ground := ⋯ }

@[simp]

theorem IndepMatroid.matroid_E {α : Type u_1} (M : IndepMatroid α) : M.matroid.E = M.E

@[simp]

theorem IndepMatroid.matroid_IsBase {α : Type u_1} (M : IndepMatroid α) (x : Set α) : M.matroid.IsBase x = Maximal M.Indep x

@[simp]

theorem IndepMatroid.matroid_Indep {α : Type u_1} (M : IndepMatroid α) (a✝ : Set α) : M.matroid.Indep a✝ = M.Indep a✝

@[simp]

theorem IndepMatroid.matroid_indep_iff {α : Type u_1} {M : IndepMatroid α} {I : Set α} : M.matroid.Indep I ↔ M.Indep I

def IndepMatroid.ofFinitary {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : IndepMatroid α

If Indep has the 'compactness' property that each set I satisfies Indep I if and only if Indep J for every finite subset J of I, then an IndepMatroid can be constructed without proving the maximality axiom. This needs choice, since it can be used to prove that every vector space has a basis.

Equations

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

@[simp]

theorem IndepMatroid.ofFinitary_E {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E

@[simp]

theorem IndepMatroid.ofFinitary_indep {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep

instance IndepMatroid.ofFinitary_finitary {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Finitary

def IndepMatroid.ofFinitaryCardAugment {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : IndepMatroid α

An independence predicate satisfying the finite matroid axioms determines a matroid, provided independence is determined by its behaviour on finite sets.

Equations

• IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground = IndepMatroid.ofFinitary E Indep indep_empty indep_subset ⋯ indep_compact subset_ground

@[simp]

theorem IndepMatroid.ofFinitaryCardAugment_E {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E

@[simp]

theorem IndepMatroid.ofFinitaryCardAugment_indep {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep

instance IndepMatroid.ofFinitaryCardAugment_finitary {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Finitary

theorem Matroid.existsMaximalSubsetProperty_of_bdd {α : Type u_1} {P : Set α → Prop} (hP : ∃ (n : ℕ), ∀ (Y : Set α), P Y → Y.encard ≤ ↑n) (X : Set α) : ExistsMaximalSubsetProperty P X

If there is an absolute upper bound on the size of a set satisfying P, then the maximal subset property always holds.

def IndepMatroid.ofBdd {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) : IndepMatroid α

If there is an absolute upper bound on the size of an independent set, then the maximality axiom isn't needed to define a matroid by independent sets.

Equations

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

@[simp]

theorem IndepMatroid.ofBdd_E {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground indep_bdd).E = E

@[simp]

theorem IndepMatroid.ofBdd_indep {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).Indep = Indep

instance IndepMatroid.instRankFiniteMatroidOfBdd {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite

IndepMatroid.ofBdd constructs a RankFinite matroid.

def IndepMatroid.ofBddAugment {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : IndepMatroid α

If there is an absolute upper bound on the size of an independent set, then matroids can be defined using an 'augmentation' axiom similar to the standard definition of finite matroids for independent sets.

Equations

• IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground = IndepMatroid.ofBdd E Indep indep_empty indep_subset ⋯ subset_ground indep_bdd

@[simp]

theorem IndepMatroid.ofBddAugment_E {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E

@[simp]

theorem IndepMatroid.ofBddAugment_indep {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).Indep = Indep

instance IndepMatroid.ofBddAugment_rankFinite {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) : (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid.RankFinite

def IndepMatroid.ofFinite {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E) : IndepMatroid α

If E is finite, then any collection of subsets of E satisfying the usual independence axioms determines a matroid

Equations

• IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground = IndepMatroid.ofBddAugment E Indep indep_empty indep_subset ⋯ ⋯ subset_ground

@[simp]

theorem IndepMatroid.ofFinite_E {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E) : (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).E = E

@[simp]

theorem IndepMatroid.ofFinite_indep {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E) : (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).Indep = Indep

instance IndepMatroid.ofFinite_finite {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E) : (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).matroid.Finite

def IndepMatroid.ofFinset {α : Type u_1} [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) : IndepMatroid α

An independence predicate on Finset α that obeys the finite matroid axioms determines a finitary matroid on α.

Equations

• IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground = IndepMatroid.ofFinitaryCardAugment E (fun (I : Set α) => ∀ (J : Finset α), ↑J ⊆ I → Indep J) ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem IndepMatroid.ofFinset_E {α : Type u_1} [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) : (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E

@[simp]

theorem IndepMatroid.ofFinset_indep {α : Type u_1} [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 : Finset α} : (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I

theorem IndepMatroid.ofFinset_indep' {α : Type u_1} [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 can't be @[simp], because it would cause the more useful Matroid.ofIndepFinset_apply not to be in simp normal form.

def Matroid.ofExistsMatroid {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I) : Matroid α

Construct an Matroid from an independence predicate that agrees with that of some matroid M. This is computable even if M is only known existentially, or when M exists for different reasons in different cases. This can also be used to change the independence predicate to a more useful definitional form.

Equations

• Matroid.ofExistsMatroid E Indep hM = (let_fun hex := ⋯; { E := E, Indep := Indep, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }).matroid

@[simp]

theorem Matroid.ofExistsMatroid_E {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I) : (Matroid.ofExistsMatroid E Indep hM).E = E

def Matroid.ofBase {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (maximality : ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) => ∃ (B : Set α), IsBase B ∧ x ⊆ B) X) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : Matroid α

A matroid defined purely in terms of its bases.

Equations

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

@[simp]

theorem Matroid.ofBase_E {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (maximality : ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) => ∃ (B : Set α), IsBase B ∧ x ⊆ B) X) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofBase E IsBase exists_isBase isBase_exchange maximality subset_ground).E = E

def Matroid.ofExistsFiniteIsBase {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : Matroid α

A collection of bases with the exchange property and at least one finite member is a matroid

Equations

• Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground = Matroid.ofBase E IsBase ⋯ isBase_exchange ⋯ subset_ground

@[simp]

theorem Matroid.ofExistsFiniteIsBase_E {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).E = E

@[simp]

theorem Matroid.ofExistsFiniteIsBase_isBase {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).IsBase = IsBase

instance Matroid.ofExistsFiniteIsBase_rankFinite {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite

def Matroid.ofIsBaseOfFinite {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : Matroid α

If E is finite, then any nonempty collection of its subsets with the exchange property is the collection of bases of a matroid on E.

Equations

• Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground = Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground

@[simp]

theorem Matroid.ofIsBaseOfFinite_E {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).E = E

@[simp]

theorem Matroid.ofIsBaseOfFinite_isBase {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).IsBase = IsBase

instance Matroid.ofBaseOfFinite_finite {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E) : (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).Finite