OAI/Analysis/CircleDomains/Topology/CircleArgumentOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Normalize the argument of the actual centered collar boundary by its first value. Its real lift runs once around the circle, in one of the two orientations; no differentiability of the centered Jordan map is assumed.

  1. theorem OAI.CircleDomainRigidity.normalizedArgument_injective_on_unit_sphere line 17
  2. theorem OAI.CircleDomainRigidity.normalizedArgument_div line 24
  3. theorem OAI.CircleDomainRigidity.exists_ordered_argument_lift line 31
  4. theorem OAI.CircleDomainRigidity.exists_ordered_centered_collar_boundary_lift line 60