OAI/Analysis/RieszRectifiability/Surfaces/ContinuousChartInnerCoverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inner projection coverage of continuous charts

A chart whose projected displacement is small covers an inner ball in the plane direction. Bounds on the chart height and the base point's distance to the plane keep the covering points inside the required ambient ball.

  1. theorem OAI.RieszRectifiability.continuous_chart_inner_projection_coverage line 21