OAI/Combinatorics/HalvingLines/Decomposition.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Sweep.state_eq_insert_below line 10
  2. lemma OAI.PlanarHalving.Sweep.states_change_of_pair line 22
  3. def OAI.PlanarHalving.Sweep.switchPairs line 54
  4. lemma OAI.PlanarHalving.Sweep.mem_switchPairs line 57
  5. def OAI.PlanarHalving.Sweep.States.changeSteps line 62
  6. lemma OAI.PlanarHalving.Sweep.States.mem_changeSteps line 65
  7. lemma OAI.PlanarHalving.Sweep.switchCount_le_changes line 70
  8. lemma OAI.PlanarHalving.Sweep.local_change_event line 93
  9. def OAI.PlanarHalving.Sweep.subsetIndex line 137
  10. lemma OAI.PlanarHalving.Sweep.subsetIndex_strictMono line 140
  11. lemma OAI.PlanarHalving.Sweep.subsetIndex_mem line 143
  12. lemma OAI.PlanarHalving.Sweep.subsetIndex_surj line 146
  13. def OAI.PlanarHalving.Sweep.subsetPoints line 150
  14. lemma OAI.PlanarHalving.Sweep.subsetPoints_generic line 153
  15. def OAI.PlanarHalving.Sweep.restrictMarks line 156
  16. lemma OAI.PlanarHalving.Sweep.mem_restrictMarks line 159
  17. lemma OAI.PlanarHalving.Sweep.card_restrictMarks line 164
  18. lemma OAI.PlanarHalving.Sweep.restrictMarks_separates line 178
  19. lemma OAI.PlanarHalving.Sweep.Refines.subset line 184
  20. lemma OAI.PlanarHalving.Sweep.States.restrict_activity_card line 189
  21. lemma OAI.PlanarHalving.Sweep.States.restrict_activity_change line 209
  22. def OAI.PlanarHalving.Sweep.States.blockSteps line 224
  23. lemma OAI.PlanarHalving.Sweep.States.mem_blockSteps line 227
  24. lemma OAI.PlanarHalving.Sweep.card_le_of_injective_labels line 232
  25. lemma OAI.PlanarHalving.Sweep.block_step_event line 244
  26. lemma OAI.PlanarHalving.Sweep.block_count_le line 265
  27. lemma OAI.PlanarHalving.Sweep.States.blockSteps_self line 289
  28. lemma OAI.PlanarHalving.Sweep.States.blockSteps_all line 296
  29. lemma OAI.PlanarHalving.Sweep.States.blockSteps_card_add line 301
  30. lemma OAI.PlanarHalving.Sweep.States.sum_blockSteps line 324
  31. def OAI.PlanarHalving.Sweep.States.ActivityGreedy.fullIndex line 337
  32. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.fullIndex_mono line 341
  33. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.fullIndex_first line 354
  34. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.fullIndex_last line 358
  35. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.fullIndex_activity line 361
  36. lemma OAI.PlanarHalving.Sweep.activity_decomposition line 368
  37. lemma OAI.PlanarHalving.Sweep.division_scale line 400
  38. lemma OAI.PlanarHalving.Sweep.greedy_count_bound line 416
  39. lemma OAI.PlanarHalving.Sweep.recurrence_exponent line 438