OAI/Analysis/CircleDomains/Reflection/RegularPhaseSides.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two sides of the limiting analytic boundary keep their exact inside/outside assignment. The bounds are passed from the actual finite maps.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.outer_le line 18
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.inner_le line 29
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.outer_strict line 39
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.inner_strict line 48
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.boundary_iff line 57