OAI/Analysis/CircleDomains/Reflection/InjectiveModulusContinuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual boundary continuation is locally injective and has no critical boundary point when the original upper-side map is injective.

  1. lemma OAI.CircleDomainRigidity.exists_injective_continuation_of_modulus_trace_sides line 13
  2. lemma OAI.CircleDomainRigidity.exists_injective_continuation_of_modulus_trace line 87