OAI/Geometry/IsometricImmersion/Coordinates/RoundDisk.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.roundRadiusSq line 15
  2. def OAI.SmoothLocal.Geometry.roundClosedDisk line 18
  3. def OAI.SmoothLocal.Geometry.roundOpenDisk line 21
  4. def OAI.SmoothLocal.Geometry.euclideanPlaneCoordinates line 24
  5. theorem OAI.SmoothLocal.Geometry.euclideanPlaneCoordinates_dist_sq line 27
  6. theorem OAI.SmoothLocal.Geometry.roundClosedDisk_eq_preimage_closedBall line 33
  7. theorem OAI.SmoothLocal.Geometry.roundOpenDisk_eq_preimage_ball line 43
  8. theorem OAI.SmoothLocal.Geometry.isCompact_roundClosedDisk line 53
  9. theorem OAI.SmoothLocal.Geometry.interior_roundClosedDisk line 59
  10. theorem OAI.SmoothLocal.Geometry.center_mem_interior_roundClosedDisk line 68
  11. theorem OAI.SmoothLocal.Geometry.interior_roundClosedDisk_nonempty line 73
  12. theorem OAI.SmoothLocal.Geometry.mem_frontier_roundClosedDisk_iff line 77
  13. theorem OAI.SmoothLocal.Geometry.coordinateCircle_mem_roundClosedDisk line 88
  14. theorem OAI.SmoothLocal.Geometry.coordinateCircle_mem_frontier_roundClosedDisk line 93
  15. theorem OAI.SmoothLocal.Geometry.exists_coordinateCircle_of_roundRadiusSq_eq line 99
  16. theorem OAI.SmoothLocal.Geometry.exists_coordinateCircle_of_mem_frontier_roundClosedDisk line 119
  17. theorem OAI.SmoothLocal.Geometry.frontier_roundClosedDisk_eq_range line 125