OAI/Geometry/BallPacking/Layers/ParametricNestedDisks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding line 17
  2. def OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.carrier line 35
  3. def OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.NestedOn line 38
  4. def OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.eval line 41
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.eval_carrier line 54
  6. def OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.pull line 57
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.pull_radius line 86
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.pull_carrier line 89
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.nested_pull line 94
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.supported_homeomorph_image line 104
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_nested_disk_family_transport line 122
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_ordinary_nested_disk_family line 193
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_nested_disk_family line 237
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_disk_representative line 283
  15. def OAI.PackingSufficiencySupport.Hamiltonian.ParametricDiskEmbedding.restrictParam line 351
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_disk_germs line 367
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_plane_disk_germs line 430
  18. theorem OAI.PackingSufficiencySupport.Comparison.exists_positive_area_grid line 500