OAI/Geometry/RCD/Sobolev/LipschitzMetricTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transferring Lipschitz functions across approximate metric coordinates

The infimum extension has the exact target Lipschitz constant. An additive metric error only changes its values on the coordinate image by that error. This supplies continuous functions on a common Euclidean domain for local harmonic compactness.

  1. theorem OAI.RegularPointCoordinates.exists_lipschitz_metric_transfer line 20