OAI/Geometry/BallPacking/Toric/StationaryManifoldPullback.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullback_of_stationary_germ line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.image_eq_of_fixed_complement line 38
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.image_interior_eq_of_inverse line 51
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontal_compact_moser line 69
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontal_moser_endpoint line 150
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPath_isInvertible_annular line 194
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_differential_eq line 246
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_covectors_commute line 255
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_twoCovectorForm_isInvertible line 274
  10. def OAI.PackingSufficiencySupport.Hamiltonian.toricHorizontalCoefficient line 282
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHorizontalCoefficient_smooth line 286
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHorizontalCoefficient_vertical line 291
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_horizontalCoupling_isInvertible line 299
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHorizontalCoefficient_contDiffAt line 313
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHorizontalCoefficient_base line 321
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_horizontalCoupling_isInvertible_local line 332
  17. def OAI.PackingSufficiencySupport.Hamiltonian.toricChartA line 366
  18. def OAI.PackingSufficiencySupport.Hamiltonian.toricChartB line 368
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricChart_coefficients_smooth line 372
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricChart_curl line 383
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricChart_horizontal_pullback line 401
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalToricCoupling_isInvertible_chart line 423
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalToricCoupling_isInvertible line 454