OAI/Analysis/CircleDomains/Topology/CenteredBoundary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The positive angular parametrization and inverse of a centered Jordan boundary.

  1. theorem OAI.CircleDomainRigidity.standardCirclePoint_normalizedArgument line 15
  2. theorem OAI.CircleDomainRigidity.normalizedArgument_standardCirclePoint line 26
  3. def OAI.CircleDomainRigidity.centeredJordanBoundary line 31
  4. theorem OAI.CircleDomainRigidity.continuous_centeredJordanBoundary line 34
  5. theorem OAI.CircleDomainRigidity.centeredJordanBoundary_mem_frontier line 46
  6. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_boundary line 56
  7. theorem OAI.CircleDomainRigidity.centeredJordanBoundary_inverse line 68