Theorems · Definition · combinatorics

IndepMatroid.ofFinset

{α : Type u_1} →
  [inst : DecidableEq α] →
    (E : Set α) →
      (Indep : Finset α → Prop) →
        Indep ∅ →
          (∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I) →
            (∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
              (∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) → IndepMatroid α

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

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

3 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq