OAI/Analysis/CircleDomains/Uniformization/SphereRoundPhaseComponent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selected round component in the actual normalized sphere image.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.sphere_complement line 16
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.sphere_disk_component line 31