OAI/Analysis/CircleDomains/Topology/JordanControlNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quantitative neighborhood for simultaneous inner and outer containment of a Jordan fill. The interior anchor removes any choice of parametrization or orientation.

  1. theorem OAI.CircleDomainRigidity.exists_jordan_control_radius line 14