OAI/Dynamics/EntropyCounterexample/SphereInfinityChart.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.sphereInfinityFlipLinear line 10
  2. theorem OAI.Problem340.sphereInfinityFlipLinear_zero line 22
  3. theorem OAI.Problem340.sphereInfinityFlipLinear_one line 25
  4. theorem OAI.Problem340.sphereInfinityFlipLinear_two line 28
  5. theorem OAI.Problem340.sphereInfinityFlipLinear_involutive line 31
  6. def OAI.Problem340.sphereInfinityFlip line 35
  7. theorem OAI.Problem340.sphereInfinityFlip_involutive line 38
  8. def OAI.Problem340.sphereAtInfinity line 43
  9. theorem OAI.Problem340.sphereAtInfinity_val_zero line 46
  10. theorem OAI.Problem340.sphereAtInfinity_val_one line 51
  11. theorem OAI.Problem340.sphereAtInfinity_val_two line 56
  12. theorem OAI.Problem340.sphereAtInfinity_zero line 61
  13. theorem OAI.Problem340.contDiff_sphereAtInfinity_val line 66
  14. theorem OAI.Problem340.continuous_sphereAtInfinity line 70
  15. theorem OAI.Problem340.sphereAtInfinity_eq_sphereOfComplex_inv line 73
  16. def OAI.Problem340.chartSouthPole line 97
  17. theorem OAI.Problem340.sphereInfinityFlip_south line 99
  18. theorem OAI.Problem340.sphereInfinityFlip_north line 102
  19. def OAI.Problem340.complexInfinityCoordinate line 105
  20. theorem OAI.Problem340.complexSphereHomeomorph_infinityCoordinate line 108
  21. theorem OAI.Problem340.complexSphereHomeomorph_symm_atInfinity line 115
  22. def OAI.Problem340.sphereInfinityCoordinate line 120
  23. def OAI.Problem340.sphereInfinityCoordinateAmbient line 123
  24. theorem OAI.Problem340.sphereInfinityCoordinate_atInfinity line 126
  25. theorem OAI.Problem340.sphereAtInfinity_ne_south line 131
  26. theorem OAI.Problem340.sphereAtInfinity_sphereInfinityCoordinate line 137
  27. theorem OAI.Problem340.contDiffOn_sphereInfinityCoordinateAmbient line 147