OAI/Analysis/CircleDomains/Topology/CenteredJordanCoordinate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Centered disk coordinates for the actual spherical Jordan collars. The continuous extension is used only to push path laws to path space.

  1. def OAI.CircleDomainRigidity.centeredJordanCoordinate line 18
  2. theorem OAI.CircleDomainRigidity.sphereJordanCoordinate_norm_lt line 21
  3. theorem OAI.CircleDomainRigidity.sphereJordanCoordinate_norm_boundary line 28
  4. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_continuousOn line 37
  5. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_injOn line 44
  6. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_self line 53
  7. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_norm_le line 56
  8. theorem OAI.CircleDomainRigidity.centeredJordanCoordinate_norm_boundary line 63
  9. theorem OAI.CircleDomainRigidity.exists_centeredJordanExtension line 70