OAI/Analysis/CircleDomains/Topology/PositiveRegularJordanBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact regular-level Jordan boundary admits a positive regular parametrization, using only the retained circle classification and Green inputs.

  1. lemma OAI.CircleDomainRigidity.exists_positive_parametrization_of_regular_jordan_boundary line 13