OAI/Analysis/CircleDomains/Topology/BoundaryLiftOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An embedded circle has a monotone or antitone normalized real boundary lift, with one turn in absolute value. This fixes the orientation issue for the physical collar without differentiating its topological disk chart.

  1. theorem OAI.CircleDomainRigidity.strictMonoOn_Icc_of_continuous_strictMonoOn_Ioo line 19
  2. theorem OAI.CircleDomainRigidity.positive_boundary_lift_one_turn line 56
  3. theorem OAI.CircleDomainRigidity.boundary_lift_order_and_period line 77
  4. theorem OAI.CircleDomainRigidity.exists_ordered_circle_boundary_lift line 110