OAI/Analysis/CircleDomains/Transfer/RegularC1Chart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local C1 normal form, retaining the actual first coordinate, on the open domain of a scalar planar function.

  1. lemma OAI.CircleDomainRigidity.exists_c1_planar_level_chart line 12