OAI/Geometry/BallPacking/DiskMaps/SmoothInverse.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_inverse_on line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockGraph_linear_invertible line 57
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.parametric_inverse_on line 86
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_time_isotopy line 139
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_isotopy_extension line 173
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_embedding_isotopy_extension line 227
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_fiber_variable_smooth line 265
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_time_isotopy line 299
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_isotopy_extension line 339
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_embedding_isotopy_extension line 412
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothTransition_deriv_eq_zero line 447
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.scalar_path_sublevel_iff line 463
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockPath_sublevel_iff line 497
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_sublevel_iff line 532
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_strict_sublevel_iff line 544
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_sublevel_iff line 559