OAI/Analysis/CircleDomains/Reflection/CircleBoundaryContinuation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A map continuous up to a circular boundary and taking that boundary to a circle extends holomorphically near each finite Cayley chart point. Both coordinate changes and the extension are constructed explicitly.

  1. lemma OAI.CircleDomainRigidity.exists_unit_circle_continuation line 13