OAI/Analysis/CircleDomains/Uniformization/CyclicCircularization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fair finite schedule and simultaneous compactness of the actual round disks selected during its cycles. No assertion of limiting roundness for the later, deformed configurations is assumed here.

  1. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclicSchedule line 13
  2. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.visitTime line 15
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclicSchedule_visit line 17
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.visitTime_strictMono line 22
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_cyclic_selected_disk_limits line 28