OAI/Geometry/BallPacking/Surfaces/QuadricInfinityDiffeomorph.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart line 17
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_source line 21
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_target line 26
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_apply line 30
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_symm_apply line 34
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_smooth line 37
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realInfinityChart_symm_smooth line 53
  8. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDiffeomorph line 64
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDiffeomorph_source line 70
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDiffeomorph_target line 74
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinity_transition_differentiable line 77
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinity_transition_inverse_differentiable line 89
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDiffeomorph_positive line 97
  14. def OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart line 124
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart_smooth line 126
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart_coordinate line 129
  17. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart_derivative_leftInverse line 133
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart_derivative_injective line 143
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inclusionChart_derivative_one_ne line 152
  20. def OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain line 164
  21. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_closed line 167
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.fibre_norm_bound line 171
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_compact line 182
  24. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_nested line 213
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_cover line 221
  26. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection line 232
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection_continuous line 234
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection_proper line 237
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.square_not_locally_constant line 244
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.projectionChart_nonconstant line 258
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.projectionChart_open_at line 283
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection_open line 293
  33. def OAI.PackingSufficiencySupport.Hamiltonian.inverseComplementCutoff line 309
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverseComplementCutoff_one_near_zero line 312
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverseComplementCutoff_smooth line 323
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverseComplementCutoff_compact line 335
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverseComplementCutoff_range line 347
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_normSq_smooth line 355
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactSupport.comp_complex_normSq line 360
  40. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection_smooth line 381
  41. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff line 386
  42. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_smooth line 389
  43. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_compact line 395
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_range line 408
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_infinity line 412