OAI/Analysis/CircleDomains/Uniformization/CircularizationBoundaryImages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every boundary curve keeps its label under the actual extended one-hole circularization.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.other_boundary_image line 17
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.extended_boundary_images line 32