OAI/Combinatorics/HadwigerCounterexample/CoordinateBlocks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Blocks

  1. def OAI.HadwigerCounterexample.blockA line 15
  2. def OAI.HadwigerCounterexample.blockRay line 18
  3. theorem OAI.HadwigerCounterexample.lab_inj line 21
  4. theorem OAI.HadwigerCounterexample.joined_lab_inj line 28
  5. theorem OAI.HadwigerCounterexample.block_inj line 45
  6. theorem OAI.HadwigerCounterexample.blockRay_inj line 49
  7. theorem OAI.HadwigerCounterexample.joined_block_inj line 53
  8. theorem OAI.HadwigerCounterexample.blockRay_eval line 71
  9. theorem OAI.HadwigerCounterexample.project_pick line 75
  10. theorem OAI.HadwigerCounterexample.project_same line 87
  11. def OAI.HadwigerCounterexample.pullM line 96
  12. theorem OAI.HadwigerCounterexample.pullM_def line 98
  13. theorem OAI.HadwigerCounterexample.pull_test line 101
  14. theorem OAI.HadwigerCounterexample.pull_self_Z line 107
  15. theorem OAI.HadwigerCounterexample.pull_self_sharp line 122