OAI/Dynamics/EntropyCounterexample/SphereCharts.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.chartNorthVector line 12
  2. theorem OAI.Problem340.norm_chartNorthVector line 14
  3. theorem OAI.Problem340.chartNorthVector_ne_zero line 17
  4. def OAI.Problem340.chartNorthPole line 21
  5. theorem OAI.Problem340.mem_chartEquator_iff line 24
  6. def OAI.Problem340.chartEquatorLinearEquiv line 29
  7. def OAI.Problem340.chartEquatorEquiv line 50
  8. theorem OAI.Problem340.chartEquatorEquiv_apply line 58
  9. theorem OAI.Problem340.chartEquatorEquiv_apply_zero line 61
  10. theorem OAI.Problem340.chartEquatorEquiv_apply_one line 64
  11. theorem OAI.Problem340.chartEquatorEquiv_apply_two line 67
  12. theorem OAI.Problem340.chartEquatorEquiv_symm_apply line 70
  13. theorem OAI.Problem340.chartEquatorEquiv_symm_projection line 73
  14. theorem OAI.Problem340.sphere_val_two_eq_one_iff line 90
  15. def OAI.Problem340.sphereOfComplex line 102
  16. theorem OAI.Problem340.sphereOfComplex_val line 105
  17. theorem OAI.Problem340.sphereOfComplex_val_zero line 120
  18. theorem OAI.Problem340.sphereOfComplex_val_one line 129
  19. theorem OAI.Problem340.sphereOfComplex_val_two line 138
  20. def OAI.Problem340.sphereToComplex line 146
  21. theorem OAI.Problem340.sphereToComplex_sphereOfComplex line 149
  22. theorem OAI.Problem340.sphereOfComplex_ne_north line 155
  23. theorem OAI.Problem340.sphereOfComplex_sphereToComplex line 158
  24. theorem OAI.Problem340.continuous_sphereOfComplex line 170
  25. theorem OAI.Problem340.contDiff_sphereOfComplex_val line 174
  26. theorem OAI.Problem340.sphereOfComplex_injective line 180
  27. theorem OAI.Problem340.range_sphereOfComplex line 183
  28. def OAI.Problem340.sphereToComplexAmbient line 191
  29. theorem OAI.Problem340.sphereToComplexAmbient_formula line 194
  30. theorem OAI.Problem340.sphereToComplex_formula line 203
  31. theorem OAI.Problem340.contDiffOn_sphereToComplexAmbient line 208
  32. theorem OAI.Problem340.continuousOn_sphereToComplex line 217
  33. def OAI.Problem340.sphereComplexChart line 223
  34. def OAI.Problem340.scaledChartEquator line 237
  35. def OAI.Problem340.complexSphereHomeomorph line 241
  36. theorem OAI.Problem340.complexSphereHomeomorph_coe line 245
  37. theorem OAI.Problem340.complexSphereHomeomorph_infty line 249
  38. theorem OAI.Problem340.complexSphereHomeomorph_symm_north line 253
  39. theorem OAI.Problem340.complexSphereHomeomorph_symm_affine line 257
  40. theorem OAI.Problem340.isOpenEmbedding_sphereOfComplex line 261
  41. theorem OAI.Problem340.tendsto_sphereOfComplex_iff line 264
  42. theorem OAI.Problem340.tendsto_sphereOfComplex_north_iff line 270