Theorems · Definition · combinatorics

IndepMatroid.ofBddAugment

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

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

2 results in Mathlib

Foundations

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