OAI/Analysis/CircleDomains/Reflection/RegularJordanBoundaryChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local normal chart straightens the entire Jordan boundary, not only the chosen parameter arc. Compact parameter isolation excludes other arcs.

  1. lemma OAI.CircleDomainRigidity.exists_regular_jordan_boundary_chart line 13