OAI/Combinatorics/SharpRamsey/Learning/GreedyIndexed.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.GreedyPreparation.residual line 12
  2. def OAI.SharpLogRamsey.GreedyPreparation.cells line 16
  3. inductive OAI.SharpLogRamsey.GreedyPreparation.Complete line 20
  4. theorem OAI.SharpLogRamsey.GreedyPreparation.exists_complete line 27
  5. lemma OAI.SharpLogRamsey.GreedyPreparation.residual_subset line 45
  6. lemma OAI.SharpLogRamsey.GreedyPreparation.mem_cells_subset line 51
  7. lemma OAI.SharpLogRamsey.GreedyPreparation.cells_length line 61
  8. theorem OAI.SharpLogRamsey.GreedyPreparation.card_partition line 67
  9. lemma OAI.SharpLogRamsey.GreedyPreparation.disjoint_cells line 77
  10. lemma OAI.SharpLogRamsey.GreedyPreparation.complete_small_residual line 90
  11. lemma OAI.SharpLogRamsey.GreedyPreparation.complete_length_bound line 97
  12. lemma OAI.SharpLogRamsey.GreedyPreparation.complete_cells_rich line 107
  13. lemma OAI.SharpLogRamsey.GreedyPreparation.complete_cells_bounded line 119
  14. theorem OAI.SharpLogRamsey.GreedyPreparation.complete_nonincreasing line 133
  15. def OAI.SharpLogRamsey.GreedyPreparation.removed line 155
  16. def OAI.SharpLogRamsey.GreedyPreparation.own line 158
  17. lemma OAI.SharpLogRamsey.GreedyPreparation.residual_eq line 162
  18. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_subset line 172
  19. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_eq line 175
  20. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_cons line 182
  21. lemma OAI.SharpLogRamsey.GreedyPreparation.cell_subset_removed line 189
  22. lemma OAI.SharpLogRamsey.GreedyPreparation.own_empty_or_cell line 200
  23. lemma OAI.SharpLogRamsey.GreedyPreparation.own_subset_removed line 212
  24. lemma OAI.SharpLogRamsey.GreedyPreparation.own_card_le line 218
  25. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_card line 225
  26. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_card_eq_sum line 229
  27. theorem OAI.SharpLogRamsey.GreedyPreparation.preparation line 235
  28. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_inter_card_le line 251
  29. lemma OAI.SharpLogRamsey.GreedyPreparation.outside_first_inter_empty line 264
  30. lemma OAI.SharpLogRamsey.GreedyPreparation.outside_inter_prefix line 277
  31. lemma OAI.SharpLogRamsey.GreedyPreparation.residual_append line 312
  32. lemma OAI.SharpLogRamsey.GreedyPreparation.residual_nil line 318
  33. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_append line 320
  34. lemma OAI.SharpLogRamsey.GreedyPreparation.own_append line 336
  35. lemma OAI.SharpLogRamsey.GreedyPreparation.cells_get line 344
  36. def OAI.SharpLogRamsey.GreedyPreparation.indexedCell line 357
  37. lemma OAI.SharpLogRamsey.GreedyPreparation.indexedCell_eq line 360
  38. lemma OAI.SharpLogRamsey.GreedyPreparation.indexedCell_antitone line 365
  39. lemma OAI.SharpLogRamsey.GreedyPreparation.indexedCell_sum line 380
  40. lemma OAI.SharpLogRamsey.GreedyPreparation.residual_after_first_disjoint line 393
  41. lemma OAI.SharpLogRamsey.GreedyPreparation.removed_line_le_prefix_cell line 400
  42. lemma OAI.SharpLogRamsey.GreedyPreparation.first_containing line 413