OAI/Analysis/CircleDomains/Topology/RoundCollarPeriod.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One jointly continuous real lift on the unwrapped annulus gives the same finite period on every small concentric circle. The period need not be specified as an additional hypothesis for removing offsets.

  1. theorem OAI.CircleDomainRigidity.continuous_unitCircleParam_family line 16
  2. theorem OAI.CircleDomainRigidity.exists_constant_period_round_collars line 21