OAI/Geometry/BallPacking/Surfaces/DiagonalQuadric.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.Affine line 11
  2. def OAI.PackingSufficiencySupport.DiagonalQuadrics.equations line 13
  3. def OAI.PackingSufficiencySupport.DiagonalQuadrics.locus line 16
  4. def OAI.PackingSufficiencySupport.DiagonalQuadrics.jacobian line 18
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.jacobian_apply line 23
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.equations_contDiff line 26
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.equations_hasFDerivAt line 32
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.mem_locus line 40
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.locus_isClosed line 45
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.at_most_one_zero line 48
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.base_ne_zero_at_branch line 57
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.jacobian_surjective line 64
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.ordinary_augmented_bijective line 88
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.branch_augmented_bijective line 110
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.sqrt_sq_complex line 150
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.sqrt_of_sq_pos line 153
  17. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.sqrt_re_pos line 156
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.sqrt_contDiffAt line 161
  19. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.parameters line 168
  20. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.parameters_injective line 170
  21. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.parameters_nonzero line 176
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.parameters_zero line 184
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.parameters_one line 185
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus line 187
  25. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.minus line 188
  26. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.baseSquare line 189
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus_add_minus line 191
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus_sq_sub_minus_sq line 193
  29. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint line 198
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_zero line 203
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_one line 204
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_mem line 208
  33. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusDomain line 224
  34. def OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign line 229
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_sq line 230
  36. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_mul_self line 231
  37. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_re line 233
  38. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_im line 235
  39. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_ne_zero line 236
  40. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRoot line 238
  41. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint line 240
  42. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegion line 242
  43. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDomain line 243
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRoot_sq line 245
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint_mem line 249
  46. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint_coordinate line 257
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRoot_positive line 260
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegion_open line 265
  49. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityDomain_open line 273
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.zero_mem_infinityRegion line 276
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRoot_contDiffAt line 280
  52. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint_contDiffAt line 287
  53. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegion_contains_ball line 294
  54. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.branch_augmented_regular_bijective line 298
  55. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCoordinate line 336
  56. def OAI.PackingSufficiencySupport.DiagonalQuadrics.regularCoordinate line 340
  57. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.regularCoordinate_isOpen line 344
  58. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.regularCoordinate_bijective line 356
  59. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_regularCoordinate line 362
  60. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCoordinates line 371
  61. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCoordinates_contDiff line 374
  62. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCoordinates_hasFDerivAt line 378
  63. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_normal_straightening line 382
  64. structure OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart line 412
  65. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_normalChart_at line 418
  66. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.ambient_apply line 427
  67. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.inverse_on_slice line 432
  68. def OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceInverse line 438
  69. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceInverse_eq line 442
  70. def OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart line 446
  71. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart_apply line 490
  72. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart_source line 493
  73. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart_target line 496
  74. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart_symm_eq line 499
  75. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.sliceChart_inverse_smooth line 502
  76. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.transition_smooth line 509