OAI/Geometry/BallPacking/DiskMaps/CompactEmbeddingIsotopy.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.scalar_id_isInvertible line 17
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.smul_isInvertible line 25
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.isInvertible_injective line 31
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothlyAmbientRelated_contraction line 38
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_planar_embedding_isotopy line 75
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_fderiv_isInvertible line 168
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.map_smooth line 179
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.symm_smooth line 182
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.fderiv_isInvertible line 185
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.fderiv_smooth line 190
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.det_fderiv_pos line 200
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_det line 218
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_orientation_of_isotopy line 224
  14. structure OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily line 237
  15. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.eval line 250
  16. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.constant line 261
  17. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.refl line 271
  18. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.trans line 273
  19. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.symm line 288
  20. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.mono line 302
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.endpoint_smooth line 313
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.endpoint_inverse_smooth line 317
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_embedding_family_transport line 326
  24. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.conjugate line 362
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.conjugate_image line 379
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_plane_image_closedBall line 393
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_plane_image_ball line 411
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_plane_volume_image line 429
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.diagonalScale_injective line 438
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.diagonalScale_inv_image_closedRoundDisk line 445
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.volume_closedRoundDisk line 462
  32. def OAI.PackingSufficiencySupport.Hamiltonian.radialArea line 469
  33. def OAI.PackingSufficiencySupport.Hamiltonian.areaRadius line 471
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaRadius_pos line 473
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaRadius_sq line 476
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaRadius_strictMono line 479
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.mem_closedRoundDisk_areaRadius line 483
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.mem_roundDisk_areaRadius line 488
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.volume_closedRoundDisk_areaRadius line 493
  40. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedPolarMap line 499
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedPolarMap_injective line 502
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedPolarMap_det_pos line 508
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedPolarMap_image line 519
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.polarRoundedDisk_volume_eq line 524
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.roundedBox_nested_of_margins line 533
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedPolarFamily_smoothOn line 547