OAI/Analysis/RieszRectifiability/Surfaces/RecenteredDiskCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recentering disk charts

A chart whose projection is the identity restricts to any closed disk contained in its parameter disk. The recentered chart preserves the normal Lipschitz bound and parametrizes exactly the part of the original range over the smaller disk.

  1. theorem OAI.RieszRectifiability.exists_recentered_disk_chart line 21