OAI/Geometry/IsometricImmersion/Coordinates/OrientedCenterNets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Geometry.OrientationLabel line 13
  2. def OAI.SmoothLocal.Geometry.orientationLabelCode line 15
  3. theorem OAI.SmoothLocal.Geometry.orientationLabelCode_injective line 18
  4. def OAI.SmoothLocal.Geometry.orientedLayerIndex line 23
  5. theorem OAI.SmoothLocal.Geometry.orientedLayerIndex_injective line 26
  6. theorem OAI.SmoothLocal.Geometry.orientedLayerIndex_ge_stage line 32
  7. theorem OAI.SmoothLocal.Geometry.orientedLayerIndex_tendsto line 35
  8. def OAI.SmoothLocal.Geometry.orientedExteriorCenters line 39
  9. theorem OAI.SmoothLocal.Geometry.orientedExteriorCenters_mem_layer line 42
  10. theorem OAI.SmoothLocal.Geometry.orientedExteriorCenters_avoid_disks line 47
  11. theorem OAI.SmoothLocal.Geometry.orientedExteriorLayers_disjoint line 51
  12. theorem OAI.SmoothLocal.Geometry.every_boundary_point_every_orientation_centers line 56
  13. theorem OAI.SmoothLocal.Geometry.every_boundary_point_every_rotation_centers line 64