OAI/Geometry/RCD/Transport/PointedLocalGeodesic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Geodesic control from nearby image endpoints anywhere in the interior

  1. theorem OAI.RegularPointCoordinates.pointed_local_geodesic_within line 13
  2. theorem OAI.RegularPointCoordinates.pointed_local_geodesic_image line 38