OAI/Geometry/BallPacking/Surfaces/QuadricCurveManifold.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalChartAt line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.mem_normalChartAt line 18
  3. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.curveChartedSpace line 21
  4. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.curveComplexManifold line 27
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curve_inclusion_contMDiff line 33
  6. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.RealModel line 48
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.realChart line 50
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realChart_source line 53
  9. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.realSurfaceChartedSpace line 57
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.real_transition_smooth line 63
  11. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.realSurfaceManifold line 75
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.real_inclusion_contMDiff line 80
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curve_contMDiffWithinAt_of_ambient line 108
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.real_contMDiffWithinAt_of_ambient line 122
  15. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityBranch line 139
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalized_coordinate_sq line 142
  17. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint_inverse line 147
  18. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityFallback line 157
  19. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityInverse line 163
  20. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityInverse_val line 167
  21. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityBranch_open line 171
  22. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityChart line 190
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityChart_apply line 225
  24. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityChart_source line 226
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityChart_target line 227
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.re_ne_zero_of_sq_re_pos line 233
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endSign_positive_unique line 239
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_positive_endSign line 244
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityBranch_disjoint line 249
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_infinityBranch line 257
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityBranch_cover line 268
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.large_coordinate_in_end line 279
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinity_end_count line 289
  34. theorem OAI.PackingSufficiencySupport.complex_real_conjugate_det line 298
  35. theorem OAI.PackingSufficiencySupport.holomorphic_plane_det_nonneg line 309
  36. theorem OAI.PackingSufficiencySupport.partialHomeomorph_fderiv_det_ne_zero line 317
  37. theorem OAI.PackingSufficiencySupport.holomorphic_partialHomeomorph_orientation line 334