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 all 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.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 FiniteRk.

• 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 α.

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

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

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

structure IndepMatroid (α : Type u_2) : Type u_2

A matroid as defined by the independence axioms. This is the same thing as a Matroid, and so does not need its own API; it exists to make it easier to construct a matroid from its independent sets. The constructed IndepMatroid can then be converted into a matroid with IndepMatroid.matroid.

• 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 → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | self.Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | self.Indep I} → ∃ x ∈ B \ I, self.Indep (insert x I)
• indep_maximal : ∀ X ⊆ self.E, Matroid.ExistsMaximalSubsetProperty self.Indep X
• subset_ground : ∀ (I : Set α), self.Indep I → I ⊆ self.E

theorem IndepMatroid.indep_empty {α : Type u_2} (self : IndepMatroid α) : self.Indep ∅

theorem IndepMatroid.indep_subset {α : Type u_2} (self : IndepMatroid α) ⦃I : Set α⦄ ⦃J : Set α⦄ : self.Indep J → I ⊆ J → self.Indep I

theorem IndepMatroid.indep_aug {α : Type u_2} (self : IndepMatroid α) ⦃I : Set α⦄ ⦃B : Set α⦄ : self.Indep I → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | self.Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | self.Indep I} → ∃ x ∈ B \ I, self.Indep (insert x I)

theorem IndepMatroid.indep_maximal {α : Type u_2} (self : IndepMatroid α) (X : Set α) : X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty self.Indep X

theorem IndepMatroid.subset_ground {α : Type u_2} (self : IndepMatroid α) (I : Set α) : self.Indep I → I ⊆ self.E

@[simp]

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

@[simp]

theorem IndepMatroid.matroid_Base {α : Type u_1} (M : IndepMatroid α) : ∀ (x : Set α), M.matroid.Base x = (x ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | M.Indep I})

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

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

Equations

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

@[simp]

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

@[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 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.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E

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 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. This fundamentally 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_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.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 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.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Finitary

Equations

• ⋯ = ⋯

theorem Matroid.existsMaximalSubsetProperty_of_bdd {α : Type u_1} {P : Set α → Prop} (hP : ∃ (n : ℕ), ∀ (Y : Set α), P Y → Y.encard ≤ ↑n) (X : Set α) : Matroid.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.

@[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 → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → ∃ 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

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 → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → ∃ 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_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 → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → ∃ 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.instFiniteRkMatroidOfBdd {α : 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 → I ∉ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → B ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {I : Set α | Indep I} → ∃ 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.FiniteRk

IndepMatroid.ofBdd constructs a FiniteRk matroid.

Equations

• ⋯ = ⋯

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_finiteRk {α : 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.FiniteRk

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.ofFinitary 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.

@[simp]

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

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

Construct an IndepMatroid from an independence predicate that agrees with that of some matroid M. Computable even when M is not known constructively.

Equations

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

@[simp]

theorem Matroid.ofExistsFiniteBase_E {α : Type u_1} (E : Set α) (Base : Set α → Prop) (exists_finite_base : ∃ (B : Set α), Base B ∧ B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).E = E

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

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

Equations

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

@[simp]

theorem Matroid.ofExistsFiniteBase_base {α : Type u_1} (E : Set α) (Base : Set α → Prop) (exists_finite_base : ∃ (B : Set α), Base B ∧ B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).Base = Base

instance Matroid.ofExistsFiniteBase_finiteRk {α : Type u_1} (E : Set α) (Base : Set α → Prop) (exists_finite_base : ∃ (B : Set α), Base B ∧ B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).FiniteRk

Equations

• ⋯ = ⋯

def Matroid.ofBaseOfFinite {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set α → Prop) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base 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.ofBaseOfFinite hE Base exists_base base_exchange subset_ground = Matroid.ofExistsFiniteBase E Base ⋯ base_exchange subset_ground

@[simp]

theorem Matroid.ofBaseOfFinite_E {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set α → Prop) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).E = E

@[simp]

theorem Matroid.ofBaseOfFinite_base {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set α → Prop) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).Base = Base

instance Matroid.ofBaseOfFinite_finite {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set α → Prop) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base B → B ⊆ E) : (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).Finite

Equations

• ⋯ = ⋯