OAI/Analysis/CircleDomains/Reflection/ReflectedCircleImages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Each boundary circle has a full round-circle image under the actual principal map. Positivity of the radius follows from injectivity, and the reverse inclusion follows from the exact reflected fixed-point equation.

  1. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedLimit_fixed_iff line 17
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.exists_round_boundary_image line 34