OAI/Analysis/RieszRectifiability/Projections/CoveredProjectionCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Charts over covered projections

A cone bound makes orthogonal projection injective on the given set. Over any covered projection domain, its inverse is a Lipschitz chart whose normal component has the prescribed Lipschitz bound and whose range is exactly the corresponding slice.

  1. theorem OAI.RieszRectifiability.exists_chart_on_covered_projection line 21