OAI/Dynamics/EntropyCounterexample/SphereDoubling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SphereDoubling.Ambient line 9
  2. abbrev OAI.Problem340.SphereDoubling.Sphere line 10
  3. def OAI.Problem340.SphereDoubling.ambientMap line 12
  4. lemma OAI.Problem340.SphereDoubling.denominator_pos line 17
  5. lemma OAI.Problem340.SphereDoubling.contDiff_ambientMap line 19
  6. lemma OAI.Problem340.SphereDoubling.sphere_equation line 30
  7. lemma OAI.Problem340.SphereDoubling.ambientMap_mem_sphere line 36
  8. def OAI.Problem340.SphereDoubling.sphereMap line 48
  9. lemma OAI.Problem340.SphereDoubling.continuous_sphereMap line 50
  10. def OAI.Problem340.SphereDoubling.stereoCoordinate line 53
  11. lemma OAI.Problem340.SphereDoubling.ambientMap_third_ne_one line 56
  12. lemma OAI.Problem340.SphereDoubling.stereoCoordinate_ambientMap line 64
  13. def OAI.Problem340.SphereDoubling.north line 84
  14. def OAI.Problem340.SphereDoubling.south line 87
  15. def OAI.Problem340.SphereDoubling.east line 90
  16. def OAI.Problem340.SphereDoubling.west line 93
  17. lemma OAI.Problem340.SphereDoubling.sphereMap_north line 96
  18. lemma OAI.Problem340.SphereDoubling.sphereMap_south line 101
  19. lemma OAI.Problem340.SphereDoubling.sphereMap_east line 106
  20. lemma OAI.Problem340.SphereDoubling.sphereMap_west line 111
  21. lemma OAI.Problem340.SphereDoubling.east_ne_west line 116
  22. lemma OAI.Problem340.SphereDoubling.not_injective_sphereMap line 121
  23. lemma OAI.Problem340.SphereDoubling.eq_north_iff line 125
  24. lemma OAI.Problem340.SphereDoubling.sphereMap_eq_north_iff line 139
  25. lemma OAI.Problem340.SphereDoubling.stereoCoordinate_sphereMap line 149
  26. lemma OAI.Problem340.SphereDoubling.iterate_sphereMap_eq_north_iff line 153
  27. lemma OAI.Problem340.SphereDoubling.stereoCoordinate_iterate_sphereMap line 159