OAI/Geometry/IsometricImmersion/Coordinates/ExteriorAnnuli.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.roundDistance line 11
  2. theorem OAI.SmoothLocal.Geometry.roundDistance_sq line 14
  3. theorem OAI.SmoothLocal.Geometry.roundDistance_nonneg line 17
  4. theorem OAI.SmoothLocal.Geometry.roundDistance_continuous line 19
  5. theorem OAI.SmoothLocal.Geometry.mem_roundClosedDisk_iff_roundDistance line 22
  6. theorem OAI.SmoothLocal.Geometry.mem_roundOpenDisk_iff_roundDistance line 27
  7. theorem OAI.SmoothLocal.Geometry.frontier_roundDistance_eq line 32
  8. def OAI.SmoothLocal.Geometry.exteriorLayerInner line 38
  9. def OAI.SmoothLocal.Geometry.exteriorLayerOuter line 41
  10. def OAI.SmoothLocal.Geometry.exteriorLayerMiddle line 44
  11. def OAI.SmoothLocal.Geometry.exteriorClosedLayer line 47
  12. def OAI.SmoothLocal.Geometry.exteriorOpenLayer line 51
  13. theorem OAI.SmoothLocal.Geometry.exteriorLayer_radii line 55
  14. theorem OAI.SmoothLocal.Geometry.exteriorLayer_clearances line 71
  15. theorem OAI.SmoothLocal.Geometry.exteriorOpenLayer_isOpen line 87
  16. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayer_isClosed line 91
  17. theorem OAI.SmoothLocal.Geometry.exteriorOpenLayer_subset_closed line 95
  18. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayer_outside_disk line 98
  19. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayer_subset_enlarged_open line 106
  20. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayer_subset_enlarged line 114
  21. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayer_isCompact line 121
  22. theorem OAI.SmoothLocal.Geometry.exteriorLayer_separated line 125
  23. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayers_pairwise_disjoint line 133
  24. theorem OAI.SmoothLocal.Geometry.exteriorClosedLayers_disjoint_different_disks line 142
  25. def OAI.SmoothLocal.Geometry.radialLift line 147
  26. theorem OAI.SmoothLocal.Geometry.roundDistance_radialLift line 149
  27. def OAI.SmoothLocal.Geometry.exteriorMiddleLift line 154
  28. theorem OAI.SmoothLocal.Geometry.exteriorMiddleLift_mem_layer line 157
  29. theorem OAI.SmoothLocal.Geometry.exteriorMiddleLift_tendsto line 173
  30. theorem OAI.SmoothLocal.Geometry.every_disk_boundary_has_exterior_layer_sequence line 184