OAI/Analysis/CircleDomains/Modulus/NormalizedArgument.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Circular argument in turns, and continuous argument increments of paths avoiding a moving point. These use the existing real covering map.

  1. abbrev OAI.CircleDomainRigidity.FiniteTransfer.AvoidingPathPoint line 17
  2. def OAI.CircleDomainRigidity.FiniteTransfer.pathArgument line 19
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_pathArgument line 27
  4. def OAI.CircleDomainRigidity.FiniteTransfer.pathArgumentIncrement line 40
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_pathArgumentIncrement line 42
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.pathArgumentIncrement_projects line 45
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.pathArgumentIncrement_integer_of_closed line 52