OAI/Combinatorics/InfiniteMatroid/Zones.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.slice line 11
  2. lemma OAI.InfiniteMatroidCounterexample.slice_compl line 12
  3. lemma OAI.InfiniteMatroidCounterexample.slice_symmDiff line 13
  4. lemma OAI.InfiniteMatroidCounterexample.slice_empty line 14
  5. lemma OAI.InfiniteMatroidCounterexample.slice_univ line 15
  6. lemma OAI.InfiniteMatroidCounterexample.slice_mono line 16
  7. lemma OAI.InfiniteMatroidCounterexample.subset_iff_slice line 17
  8. def OAI.InfiniteMatroidCounterexample.joinSlices line 22
  9. lemma OAI.InfiniteMatroidCounterexample.slice_join_false line 23
  10. lemma OAI.InfiniteMatroidCounterexample.slice_join_true line 24
  11. lemma OAI.InfiniteMatroidCounterexample.density_slice_le line 26
  12. lemma OAI.InfiniteMatroidCounterexample.small_slice line 44
  13. def OAI.InfiniteMatroidCounterexample.KSmall0 line 48
  14. lemma OAI.InfiniteMatroidCounterexample.small_kSmall0 line 49
  15. lemma OAI.InfiniteMatroidCounterexample.kSmall0_mono line 50
  16. lemma OAI.InfiniteMatroidCounterexample.kSmall0_union line 52
  17. lemma OAI.InfiniteMatroidCounterexample.hCell_kSmall0 line 54
  18. def OAI.InfiniteMatroidCounterexample.RankModel.Admissible line 61
  19. def OAI.InfiniteMatroidCounterexample.RankModel.Upper line 66
  20. def OAI.InfiniteMatroidCounterexample.RankModel.Lower line 69
  21. lemma OAI.InfiniteMatroidCounterexample.RankModel.admissible_iff line 71
  22. lemma OAI.InfiniteMatroidCounterexample.RankModel.admissible_compl line 75
  23. lemma OAI.InfiniteMatroidCounterexample.RankModel.upper_mono line 79
  24. lemma OAI.InfiniteMatroidCounterexample.RankModel.lower_mono line 90
  25. lemma OAI.InfiniteMatroidCounterexample.RankModel.upper_univ line 93
  26. lemma OAI.InfiniteMatroidCounterexample.RankModel.lower_empty line 95
  27. lemma OAI.InfiniteMatroidCounterexample.RankModel.upper_not_lower line 96
  28. lemma OAI.InfiniteMatroidCounterexample.RankModel.not_upper_empty line 100
  29. lemma OAI.InfiniteMatroidCounterexample.RankModel.not_lower_univ line 101
  30. lemma OAI.InfiniteMatroidCounterexample.RankModel.status_invariant line 105
  31. lemma OAI.InfiniteMatroidCounterexample.RankModel.admissible_positive line 139
  32. lemma OAI.InfiniteMatroidCounterexample.RankModel.admissible_sameClass line 146
  33. lemma OAI.InfiniteMatroidCounterexample.RankModel.zone_crossing line 153
  34. lemma OAI.InfiniteMatroidCounterexample.RankModel.exists_admissible_between line 186