OAI/Geometry/RCD/Metric/PointedFunctionCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform function compactness on varying pointed balls

The source functions are compared through the prescribed metric maps. The limit is a genuine Lipschitz function on Euclidean space, and the convergence is uniform on each physical source ball in this statement.

  1. theorem OAI.RegularPointCoordinates.pointed_function_compactness line 19