Theorems · Definition · combinatorics

IndepMatroid.ofFinitaryCardAugment

{α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I J : Set α⦄,
              Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
            (∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) → (∀ (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.

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

4 results in Mathlib

Foundations

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