OAI/Analysis/CircleDomains/Topology/OrderedCollarLift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A jointly lifted physical collar, normalized at the boundary. All fields below are constructed from the regular collar and its actual disk coordinate; in particular, positive winding is not an input assumption.

  1. structure OAI.CircleDomainRigidity.OrderedCollarLift line 16
  2. theorem OAI.CircleDomainRigidity.exists_ordered_collar_lift_of_parameter line 36
  3. theorem OAI.CircleDomainRigidity.exists_ordered_collar_lift line 83
  4. def OAI.CircleDomainRigidity.OrderedCollarLift.circuit line 96
  5. theorem OAI.CircleDomainRigidity.OrderedCollarLift.circuit_smooth line 100
  6. theorem OAI.CircleDomainRigidity.OrderedCollarLift.circuit_periodic line 105
  7. theorem OAI.CircleDomainRigidity.OrderedCollarLift.circuit_mem_frontier line 110
  8. theorem OAI.CircleDomainRigidity.OrderedCollarLift.abs_circleFormIntegral line 115
  9. theorem OAI.CircleDomainRigidity.OrderedCollarLift.continuous_slice line 122
  10. theorem OAI.CircleDomainRigidity.OrderedCollarLift.inverse_angle_mem line 128
  11. theorem OAI.CircleDomainRigidity.OrderedCollarLift.boundary_identification line 137