OAI/Analysis/RieszRectifiability/Foundations/BallLipschitzExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional Lipschitz extension turns partial parameterizations into maps on entire balls while retaining their images and controlling the Lipschitz constant.

  1. theorem OAI.RieszRectifiability.exists_ball_lipschitz_extension line 18
  2. theorem OAI.RieszRectifiability.uniformlyRectifiable_of_partial_parameterizations line 28