OAI/Combinatorics/HadwigerCounterexample/RandomLinearTransforms.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Random Linear Transforms

  1. instance OAI.HadwigerCounterexample.Move.finiteMove line 16
  2. instance OAI.HadwigerCounterexample.Move.identity_move line 26
  3. def OAI.HadwigerCounterexample.Move.combine line 28
  4. theorem OAI.HadwigerCounterexample.Move.extn line 32
  5. def OAI.HadwigerCounterexample.Move.circShift line 34
  6. def OAI.HadwigerCounterexample.Move.flipLines line 41
  7. theorem OAI.HadwigerCounterexample.Move.flit_obs line 47
  8. theorem OAI.HadwigerCounterexample.Move.flit_pmax line 59
  9. def OAI.HadwigerCounterexample.Move.plume line 79
  10. theorem OAI.HadwigerCounterexample.Move.plume_dim line 82
  11. theorem OAI.HadwigerCounterexample.Move.smaller_cols line 87
  12. theorem OAI.HadwigerCounterexample.Move.plume_meets line 96