OAI/Analysis/CircleDomains/Topology/BoundaryOrderExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extend the increasing boundary-angle parametrization of the unit interval to an order isomorphism of the real line. Its outside values are irrelevant to the boundary pairing.

  1. theorem OAI.CircleDomainRigidity.exists_boundary_orderIso line 15