OAI/Analysis/CircleDomains/Reflection/InjectiveAnalyticCircularization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual cyclic boundary continuations are injective, with nonzero derivative at every point of their open domains.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.injective_analytic_boundary_continuation line 17
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclic_stage_injective_boundary_continuation line 35