OAI/Analysis/CircleDomains/Topology/CircleIncrementContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous families of circle paths have continuous real increments. This follows from the actual homotopy lift, so no choice of a discontinuous starting-angle representative enters the continuity or compact bounds.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_family_circle_increment line 15
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_circlePathIncrement line 36
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.compact_circle_increment_bounded line 61