OAI/Analysis/CircleDomains/Sobolev/SmoothRadialShrinkInverse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The radial contraction has an everywhere invertible differential, so its actual global inverse is smooth.

  1. lemma OAI.CircleDomainRigidity.radialShrink_fderiv_injective line 16
  2. lemma OAI.CircleDomainRigidity.smoothRadialShrinkHomeomorph_inverse_contDiff line 60