OAI/Geometry/CubicTorus/Profiles/TransverseTorus.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.axialProjection_axis line 13
  2. lemma OAI.CubicTorus.sibling_axialProjection_idempotent line 16
  3. lemma OAI.CubicTorus.axialProjection_transverse line 21
  4. lemma OAI.CubicTorus.axialProjection_coordinates line 26
  5. lemma OAI.CubicTorus.axialCylinder_preconnected line 32
  6. theorem OAI.CubicTorus.sibling_closed_cylindrical_set_contains_cylinder line 61
  7. lemma OAI.CubicTorus.coordinate_axialProjection_lattice line 117
  8. theorem OAI.CubicTorus.periodic_complete_coordinate_cylinder_radius_lt_half line 127
  9. theorem OAI.CubicTorus.periodic_connected_coordinate_cylindrical_boundary line 193
  10. lemma OAI.CubicTorus.isMinimizerAt_zero_component_multiplier_ne_zero line 253
  11. theorem OAI.CubicTorus.isMinimizerAt_zero_axis_cylindrical_boundary line 280
  12. def OAI.CubicTorus.transverseTorus line 331
  13. lemma OAI.CubicTorus.transverseTorus_apply line 334
  14. lemma OAI.CubicTorus.continuous_transverseTorus line 337
  15. lemma OAI.CubicTorus.coordinate_axialProjection_apply line 345
  16. lemma OAI.CubicTorus.transverseTorus_quotientMap line 353
  17. lemma OAI.CubicTorus.transverseTorus_add line 359
  18. lemma OAI.CubicTorus.transverseTorus_sub line 363
  19. lemma OAI.CubicTorus.norm_transverseTorus_shortestLift line 367
  20. lemma OAI.CubicTorus.quotientMap_image_coordinate_cylinder line 377
  21. lemma OAI.CubicTorus.torus_solid_cylinder_preconnected line 401
  22. theorem OAI.CubicTorus.torus_cylinder_exterior_preconnected line 432
  23. theorem OAI.CubicTorus.isMinimizerAt_two_connected_phases line 536
  24. lemma OAI.CubicTorus.torus_preconnected_sub_preimage line 579
  25. def OAI.CubicTorus.coordinateTube line 601
  26. lemma OAI.CubicTorus.isOpen_coordinateTube line 604
  27. theorem OAI.CubicTorus.isMinimizerAt_coordinate_cylinder_phase line 608
  28. def OAI.CubicTorus.sibling_coverCoordinatePermute line 645
  29. lemma OAI.CubicTorus.sibling_coverCoordinatePermute_apply line 648
  30. lemma OAI.CubicTorus.sibling_torusCoordinatePermute_apply line 652
  31. lemma OAI.CubicTorus.coverCoordinatePermute_quotient line 655
  32. def OAI.CubicTorus.coordinatePermutation line 660
  33. lemma OAI.CubicTorus.coverCoordinatePermute_symm line 665
  34. lemma OAI.CubicTorus.torusCoordinatePermute_symm line 673
  35. theorem OAI.CubicTorus.isMinimizerAt_coordinatePermutation line 678
  36. lemma OAI.CubicTorus.transverseTorus_permute line 695
  37. lemma OAI.CubicTorus.norm_transverseTorus_zero_sq line 700
  38. lemma OAI.CubicTorus.coordinateTube_zero_eq line 705
  39. lemma OAI.CubicTorus.coordinateTube_eq_permutation_preimage line 711
  40. lemma OAI.CubicTorus.coordinateTube_eq_translate line 721
  41. lemma OAI.CubicTorus.coordinateTube_volume line 725
  42. lemma OAI.CubicTorus.coordinateTube_perimeter line 734
  43. lemma OAI.CubicTorus.small_minimizer_coordinate_tube_phase line 757
  44. lemma OAI.CubicTorus.coordinateTube_isometric_canonical line 785
  45. theorem OAI.CubicTorus.isMinimizerAt_coordinate_cylinder_standard line 804