OAI/Geometry/RCD/Metric/PointedLimitCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of local limits through a pointed approximation

Density of the prescribed coordinate maps identifies two continuous limits whenever the source representatives coincide on the interior ball.

  1. theorem OAI.RegularPointCoordinates.pointed_limits_eqOn line 17