OAI/Analysis/CircleDomains/Topology/PrincipalHomeomorphOrientation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Principal normalization gives bounded displacement on the entire plane. Its straight-line sphere homotopy supplies the orientation class used in the definition of conformal removability.

  1. theorem OAI.CircleDomainRigidity.principal_homeomorph_orientation line 13