OAI/Geometry/RCD/Transport/GeodesicProductSamples.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separated points in an approximate residual factor

Only the source space is geodesic. The residual factor is an arbitrary metric space; its separated samples are projections of one actual geodesic.

  1. theorem OAI.RegularPointCoordinates.pointed_vertical_samples line 18