OAI/Geometry/RCD/Transport/BoundedPathDistortion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reduced distortion as a bounded continuous path test

  1. def OAI.RegularPointCoordinates.pathDistortion line 14