OAI/Analysis/RieszRectifiability/Foundations/FinitePieceCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinates selected from a Lipschitz ball cover

Choosing a preimage for each covered point produces coordinates in the parameter ball. The Lipschitz bound on the covering map controls ambient distances by the distances between these selected coordinates, without requiring continuity of the selection.

  1. theorem OAI.RieszRectifiability.exists_coordinates_of_lipschitz_ball_cover line 22
  2. def OAI.RieszRectifiability.finitePartialCoordinateConstant line 44
  3. theorem OAI.RieszRectifiability.finitePartialCoordinateConstant_ge_one line 47
  4. theorem OAI.RieszRectifiability.exists_coordinates_of_finite_partial_charts line 50