OAI/Analysis/CircleDomains/Reflection/SemidiskContinuousExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The derivative estimate supplies an actual continuous extension, constructed by extending the two real Lipschitz coordinates.

  1. lemma OAI.CircleDomainRigidity.exists_continuous_extension_of_lipschitz line 12
  2. lemma OAI.CircleDomainRigidity.semidisk_continuous_extension line 26