OAI/Geometry/RCD/Coordinates/FrameVelocityErrorLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normalized velocity errors from the original spatial estimates

  1. theorem OAI.RegularPointCoordinates.frame_velocity_error_tendsto line 15