OAI/Combinatorics/InfiniteMatroid/DensityIdeal.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InfiniteMatroidCounterexample.signed_columns_positive line 12
  2. def OAI.InfiniteMatroidCounterexample.tagA line 29
  3. def OAI.InfiniteMatroidCounterexample.tagB line 30
  4. def OAI.InfiniteMatroidCounterexample.tagG line 31
  5. def OAI.InfiniteMatroidCounterexample.AColumn line 32
  6. def OAI.InfiniteMatroidCounterexample.BColumn line 33
  7. def OAI.InfiniteMatroidCounterexample.GColumn line 34
  8. def OAI.InfiniteMatroidCounterexample.Ameet line 36
  9. def OAI.InfiniteMatroidCounterexample.KSmall line 37
  10. lemma OAI.InfiniteMatroidCounterexample.Ameet_union line 39
  11. lemma OAI.InfiniteMatroidCounterexample.dSmall_kSmall line 48
  12. lemma OAI.InfiniteMatroidCounterexample.kSmall_mono line 52
  13. lemma OAI.InfiniteMatroidCounterexample.kSmall_union line 56
  14. lemma OAI.InfiniteMatroidCounterexample.Ameet_positive line 67
  15. lemma OAI.InfiniteMatroidCounterexample.kSmall_proper line 73
  16. def OAI.InfiniteMatroidCounterexample.KIdeal line 77
  17. lemma OAI.InfiniteMatroidCounterexample.AColumn_compl_kSmall line 81
  18. lemma OAI.InfiniteMatroidCounterexample.Gpattern_kPositive line 88
  19. lemma OAI.InfiniteMatroidCounterexample.exists_concrete_rank line 117