OAI/Analysis/RieszRectifiability/Surfaces/RescaledBallCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A Lipschitz chart on a centered ball can be translated and rescaled without changing its image. Rescaling the parameter ball by the inverse factor multiplies the Lipschitz bound by that factor.

  1. theorem OAI.RieszRectifiability.exists_rescaled_ball_chart line 18