OAI/Combinatorics/HalvingLines/Greedy.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Generic.comp_strictMono line 10
  2. lemma OAI.PlanarHalving.Sweep.States.outside_activity_constant line 28
  3. lemma OAI.PlanarHalving.Sweep.States.intervalActivity_self line 36
  4. lemma OAI.PlanarHalving.Sweep.States.intervalActivity_mono line 46
  5. lemma OAI.PlanarHalving.Sweep.States.intervalActivity_step_subset line 53
  6. lemma OAI.PlanarHalving.Sweep.States.intervalActivity_step_card line 72
  7. def OAI.PlanarHalving.Sweep.States.activitySize line 91
  8. lemma OAI.PlanarHalving.Sweep.States.activitySize_eq line 94
  9. lemma OAI.PlanarHalving.Sweep.States.activitySize_self line 97
  10. def OAI.PlanarHalving.Sweep.States.activityEligible line 100
  11. def OAI.PlanarHalving.Sweep.States.activityNext line 103
  12. lemma OAI.PlanarHalving.Sweep.States.activityNext_spec line 106
  13. lemma OAI.PlanarHalving.Sweep.States.before_activityNext line 110
  14. lemma OAI.PlanarHalving.Sweep.States.activityNext_bound line 120
  15. structure OAI.PlanarHalving.Sweep.States.ActivityGreedy line 131
  16. def OAI.PlanarHalving.Sweep.States.activityGreedy line 140
  17. def OAI.PlanarHalving.Sweep.States.ActivityGreedy.intervals line 176
  18. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.intervals_card line 180
  19. lemma OAI.PlanarHalving.Sweep.States.ActivityGreedy.intervals_data line 187
  20. lemma OAI.PlanarHalving.Sweep.continuous_lt_iff_of_no_eq line 209
  21. lemma OAI.PlanarHalving.Sweep.projection_eq_iff_slope line 223
  22. lemma OAI.PlanarHalving.Sweep.tied_projection line 229
  23. lemma OAI.PlanarHalving.Sweep.Traversal.cut_bounds line 235
  24. lemma OAI.PlanarHalving.Sweep.Traversal.projection_ne_between line 240
  25. lemma OAI.PlanarHalving.Sweep.Traversal.comparison_cut line 253
  26. lemma OAI.PlanarHalving.Sweep.projection_ne_at_pair line 269
  27. def OAI.PlanarHalving.Sweep.Refines line 287
  28. lemma OAI.PlanarHalving.Sweep.Traversal.sample_refines line 290
  29. def OAI.PlanarHalving.Sweep.belowSet line 298
  30. lemma OAI.PlanarHalving.Sweep.mem_belowSet line 301
  31. lemma OAI.PlanarHalving.Sweep.card_belowSet line 306
  32. lemma OAI.PlanarHalving.Sweep.belowSet_eq_erase line 309
  33. lemma OAI.PlanarHalving.Sweep.below_insert_separates line 332
  34. lemma OAI.PlanarHalving.Sweep.projection_order_at_slope line 350
  35. lemma OAI.PlanarHalving.Sweep.belowSet_symm line 359
  36. lemma OAI.PlanarHalving.Sweep.belowCount_symm line 365