OAI/Dynamics/EntropyCounterexample/SphereSquareEquator.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SphereDoubling.Equator line 9
  2. def OAI.Problem340.SphereDoubling.circleInclusion line 11
  3. theorem OAI.Problem340.SphereDoubling.circleInclusion_zero line 22
  4. theorem OAI.Problem340.SphereDoubling.circleInclusion_one line 23
  5. theorem OAI.Problem340.SphereDoubling.circleInclusion_two line 24
  6. lemma OAI.Problem340.SphereDoubling.continuous_circleInclusion line 26
  7. theorem OAI.Problem340.SphereDoubling.sphereMap_circleInclusion line 36
  8. def OAI.Problem340.SphereDoubling.equatorCoordinate line 44
  9. lemma OAI.Problem340.SphereDoubling.circleInclusion_equatorCoordinate line 54
  10. lemma OAI.Problem340.SphereDoubling.equatorCoordinate_circleInclusion line 60
  11. lemma OAI.Problem340.SphereDoubling.continuous_equatorCoordinate line 65
  12. def OAI.Problem340.SphereDoubling.circleEquatorHomeomorph line 79
  13. theorem OAI.Problem340.SphereDoubling.sphereMap_third_eq_zero_iff line 87
  14. theorem OAI.Problem340.SphereDoubling.sphereMap_third_pos_iff line 93
  15. theorem OAI.Problem340.SphereDoubling.sphereMap_third_neg_iff line 99
  16. def OAI.Problem340.SphereDoubling.equatorSquare line 105
  17. lemma OAI.Problem340.SphereDoubling.continuous_equatorSquare line 108
  18. theorem OAI.Problem340.SphereDoubling.equatorSquare_circleEquatorHomeomorph line 111
  19. lemma OAI.Problem340.SphereDoubling.eq_south_iff line 115
  20. theorem OAI.Problem340.SphereDoubling.sphereMap_eq_south_iff line 127
  21. theorem OAI.Problem340.SphereDoubling.sphereMap_mapsTo_puncturedNorth line 134
  22. theorem OAI.Problem340.SphereDoubling.sphereMap_mapsTo_puncturedSouth line 139