OAI/Geometry/IsometricImmersion/Coordinates/OrientedPatchSquares.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.exists_orientedPatchScale line 11
  2. def OAI.SmoothLocal.Geometry.orientedPatchScale line 23
  3. def OAI.SmoothLocal.Geometry.orientedClosedPatch line 26
  4. theorem OAI.SmoothLocal.Geometry.orientedPatchScale_pos line 29
  5. theorem OAI.SmoothLocal.Geometry.orientedPatchScale_le line 33
  6. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_subset_layer line 37
  7. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_dist_le line 42
  8. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_isCompact line 48
  9. theorem OAI.SmoothLocal.Geometry.center_mem_orientedClosedPatch line 52
  10. theorem OAI.SmoothLocal.Geometry.orientedClosedPatches_disjoint_same_layer line 56
  11. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_subset_closedLayer line 62
  12. theorem OAI.SmoothLocal.Geometry.orientedClosedPatches_disjoint_different_layers line 68
  13. theorem OAI.SmoothLocal.Geometry.orientedClosedPatches_disjoint_different_disks line 77
  14. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_disjoint_every_disk line 86
  15. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_subset_enlarged line 92
  16. theorem OAI.SmoothLocal.Geometry.orientedClosedPatch_subset_square line 98
  17. theorem OAI.SmoothLocal.Geometry.orientedPatchScale_tendsto line 103
  18. theorem OAI.SmoothLocal.Geometry.orientedPatchMatrix_isUnit line 108
  19. theorem OAI.SmoothLocal.Geometry.every_boundary_point_every_orientation_patch_neighborhoods line 115