OAI/Combinatorics/Ryser/Selection/ChunkPartition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.chunkRank line 11
  2. def OAI.RyserCoveringCounterexample.Selection.chunkCount line 14
  3. def OAI.RyserCoveringCounterexample.Selection.candidateChunk line 16
  4. def OAI.RyserCoveringCounterexample.Selection.chunkPrefix line 19
  5. theorem OAI.RyserCoveringCounterexample.Selection.chunkRank_of_mem line 22
  6. theorem OAI.RyserCoveringCounterexample.Selection.chunkRank_lt_card line 26
  7. theorem OAI.RyserCoveringCounterexample.Selection.chunkRank_injOn line 31
  8. theorem OAI.RyserCoveringCounterexample.Selection.mem_candidateChunk line 37
  9. theorem OAI.RyserCoveringCounterexample.Selection.mem_chunkPrefix line 41
  10. theorem OAI.RyserCoveringCounterexample.Selection.candidateChunk_subset line 45
  11. theorem OAI.RyserCoveringCounterexample.Selection.chunkPrefix_subset line 49
  12. theorem OAI.RyserCoveringCounterexample.Selection.candidateChunk_disjoint line 53
  13. theorem OAI.RyserCoveringCounterexample.Selection.candidateChunk_pairwise_disjoint line 61
  14. theorem OAI.RyserCoveringCounterexample.Selection.candidateChunk_card_le line 66
  15. theorem OAI.RyserCoveringCounterexample.Selection.chunkPrefix_zero line 86
  16. theorem OAI.RyserCoveringCounterexample.Selection.chunkPrefix_succ line 91
  17. theorem OAI.RyserCoveringCounterexample.Selection.disjoint_chunkPrefix_candidateChunk line 108
  18. theorem OAI.RyserCoveringCounterexample.Selection.chunkIndex_lt_count line 116
  19. theorem OAI.RyserCoveringCounterexample.Selection.chunkPrefix_count line 121
  20. theorem OAI.RyserCoveringCounterexample.Selection.biUnion_candidateChunk line 130