OAI/Dynamics/EntropyCounterexample/CircleClockDoubling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.CircleClockDoubling.AngularCircle line 10
  2. def OAI.Problem340.CircleClockDoubling.homeomorph line 12
  3. theorem OAI.Problem340.CircleClockDoubling.homeomorph_apply line 16
  4. def OAI.Problem340.CircleClockDoubling.angularDouble line 20
  5. theorem OAI.Problem340.CircleClockDoubling.continuous_angularDouble line 22
  6. def OAI.Problem340.CircleClockDoubling.clockDouble line 25
  7. theorem OAI.Problem340.CircleClockDoubling.continuous_clockDouble line 28
  8. theorem OAI.Problem340.CircleClockDoubling.homeomorph_angularDouble line 31
  9. theorem OAI.Problem340.CircleClockDoubling.clockDouble_eq_conjugateMap line 36
  10. theorem OAI.Problem340.CircleClockDoubling.clockDouble_coe line 41
  11. theorem OAI.Problem340.CircleClockDoubling.clockDouble_coordinates line 48
  12. def OAI.Problem340.CircleClockDoubling.homologyEquiv line 61
  13. theorem OAI.Problem340.CircleClockDoubling.homologyEquiv_apply line 65
  14. theorem OAI.Problem340.CircleClockDoubling.homologyEquiv_intertwines line 68
  15. theorem OAI.Problem340.CircleClockDoubling.eigenvector_transport line 74