OAI/Dynamics/EntropyCounterexample/ClockModel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.ClockModel.circleHomeomorph line 9
  2. theorem OAI.Problem340.ClockModel.circleHomeomorph_val line 16
  3. theorem OAI.Problem340.ClockModel.circleHomeomorph_coord_zero line 19
  4. theorem OAI.Problem340.ClockModel.circleHomeomorph_coord_one line 23
  5. def OAI.Problem340.ClockModel.clockHomeomorph line 27
  6. def OAI.Problem340.ClockModel.rotationAmbient line 30
  7. theorem OAI.Problem340.ClockModel.contDiff_rotationAmbient line 35
  8. def OAI.Problem340.ClockModel.clockRotation line 44
  9. theorem OAI.Problem340.ClockModel.clockRotation_val line 48
  10. theorem OAI.Problem340.ClockModel.clockHomeomorph_add line 51
  11. theorem OAI.Problem340.ClockModel.contDiff_rotationAmbient_comp line 58
  12. def OAI.Problem340.ClockModel.prependHomeomorph line 65
  13. theorem OAI.Problem340.ClockModel.prependHomeomorph_zero line 82
  14. theorem OAI.Problem340.ClockModel.prependHomeomorph_succ line 85
  15. def OAI.Problem340.ClockModel.productHomeomorph line 89
  16. theorem OAI.Problem340.ClockModel.productHomeomorph_clock line 95
  17. theorem OAI.Problem340.ClockModel.productHomeomorph_main line 100
  18. theorem OAI.Problem340.ClockModel.productHomeomorph_register line 105