OAI/Analysis/CircleDomains/Topology/CircleMobiusImage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Circle domains under the normalizing Möbius maps

Round complementary disks transform by multiplication of their defining matrices. A homeomorphic Möbius map therefore preserves circle domains. The explicit normalizer sends any prescribed sphere point to infinity.

  1. theorem OAI.CircleDomainRigidity.isCircleDomain_image_mobius line 20
  2. def OAI.CircleDomainRigidity.pointToInfinity line 40
  3. def OAI.CircleDomainRigidity.pointToInfinityMobius line 44
  4. theorem OAI.CircleDomainRigidity.pointToInfinity_eq_smul line 47
  5. theorem OAI.CircleDomainRigidity.pointToInfinity_apply_self line 56
  6. theorem OAI.CircleDomainRigidity.pointToInfinity_preserves_circleDomain line 66