OAI/Computability/PerfectCompleteness/Foundations/OddLists.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.OddLists.OddList line 14
  2. theorem OAI.PerfectCompleteness.OddLists.OddList.odd line 19
  3. theorem OAI.PerfectCompleteness.OddLists.OddList.card_le line 21
  4. theorem OAI.PerfectCompleteness.OddLists.OddList.card_pos line 23
  5. theorem OAI.PerfectCompleteness.OddLists.OddList.nonempty line 30
  6. def OAI.PerfectCompleteness.OddLists.OddList.singleton line 33
  7. theorem OAI.PerfectCompleteness.OddLists.OddList.singleton_val line 38
  8. theorem OAI.PerfectCompleteness.OddLists.OddList.nonempty_type line 41
  9. instance OAI.PerfectCompleteness.OddLists.OddList.(instance at line 45) line 45
  10. def OAI.PerfectCompleteness.OddLists.parityPushforward line 54
  11. theorem OAI.PerfectCompleteness.OddLists.mem_parityPushforward line 57
  12. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_preimage line 61
  13. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_subset_image line 72
  14. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_card_le line 78
  15. theorem OAI.PerfectCompleteness.OddLists.sum_fiber_card line 82
  16. theorem OAI.PerfectCompleteness.OddLists.mod_two_eq_odd_indicator line 86
  17. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_card_mod_two line 94
  18. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_odd line 101
  19. theorem OAI.PerfectCompleteness.OddLists.mem_parityPushforward_iff_sum line 107
  20. def OAI.PerfectCompleteness.OddLists.OddList.map line 115
  21. theorem OAI.PerfectCompleteness.OddLists.OddList.map_val line 119
  22. theorem OAI.PerfectCompleteness.OddLists.OddList.exists_preimage line 122
  23. theorem OAI.PerfectCompleteness.OddLists.OddList.exists_accepting_pair line 126
  24. theorem OAI.PerfectCompleteness.OddLists.OddList.exists_accepting_pair_of_eq line 132
  25. def OAI.PerfectCompleteness.OddLists.support line 144
  26. theorem OAI.PerfectCompleteness.OddLists.mem_support line 147
  27. theorem OAI.PerfectCompleteness.OddLists.binary_cases line 151
  28. theorem OAI.PerfectCompleteness.OddLists.support_card_cast line 155
  29. theorem OAI.PerfectCompleteness.OddLists.support_odd_of_sum_one line 165
  30. theorem OAI.PerfectCompleteness.OddLists.parityPushforward_support line 169
  31. def OAI.PerfectCompleteness.OddLists.OddList.extract line 190
  32. theorem OAI.PerfectCompleteness.OddLists.OddList.extract_valid line 194
  33. theorem OAI.PerfectCompleteness.OddLists.OddList.extract_invalid line 199
  34. def OAI.PerfectCompleteness.OddLists.OddList.extractOption line 204
  35. theorem OAI.PerfectCompleteness.OddLists.OddList.extractOption_none line 208
  36. theorem OAI.PerfectCompleteness.OddLists.OddList.extractOption_some_valid line 211
  37. def OAI.PerfectCompleteness.OddLists.OddList.defaultList line 216
  38. def OAI.PerfectCompleteness.OddLists.OddList.extractDefault line 219