OAI/Combinatorics/InfiniteMatroid/Matroid.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.IntervalAlternative line 11
  2. structure OAI.InfiniteMatroidCounterexample.BasisSystem line 16

    Source documentation

    The purely set-theoretic assumptions supplied by the prototype assembly.

    structure BasisSystem (α : Type*) where
…
  3. def OAI.InfiniteMatroidCounterexample.BasisSystem.Independent line 28
  4. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.independent_mono line 30
  5. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.maximal_of_base line 35
  6. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.exists_maximal_finite_gap line 43
  7. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.exists_maximal line 60
  8. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.exchange line 73
  9. def OAI.InfiniteMatroidCounterexample.BasisSystem.matroid line 82
  10. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.ground line 87
  11. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.isBase_iff line 88
  12. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.indep_iff line 89
  13. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.self_dual line 91
  14. lemma OAI.InfiniteMatroidCounterexample.BasisSystem.insert_indep_of_not_base line 97