OAI/Analysis/CircleDomains/Topology/PositiveJordanOrientation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every regular Jordan parametrization has one of two orientations. The fixed Green sign gives an actual positive parametrization.

  1. lemma OAI.CircleDomainRigidity.RegularJordanParametrization.injective_Ioc line 13
  2. lemma OAI.CircleDomainRigidity.RegularJordanParametrization.reverse line 33
  3. lemma OAI.CircleDomainRigidity.exists_positive_jordan_parametrization line 61