OAI/Combinatorics/HalvingLines/Basic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarHalving.critical_image_null line 7
  2. theorem OAI.PlanarHalving.orient_swap line 17
  3. theorem OAI.PlanarHalving.orient_left line 21
  4. theorem OAI.PlanarHalving.orient_right line 24
  5. theorem OAI.PlanarHalving.switchCount_zero line 28
  6. theorem OAI.PlanarHalving.switchCount_top line 32
  7. theorem OAI.PlanarHalving.orient_eq_proj_diff line 36
  8. lemma OAI.PlanarHalving.orient_zero_iff line 43
  9. lemma OAI.PlanarHalving.sideCount_add_reverse line 52
  10. lemma OAI.PlanarHalving.belowCount_eq_sideCount_of_x_lt line 91
  11. lemma OAI.PlanarHalving.belowCount_eq_sideCount_of_x_gt line 105
  12. theorem OAI.PlanarHalving.halvingCount_eq_middle_switchCount line 118