OAI/Analysis/CircleDomains/Topology/OrderedPhysicalCollar.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual centered Jordan boundary admits a smooth physical circuit whose disk angle is increasing from zero to one. Only the starting point and direction of the original regular circuit are changed.

  1. def OAI.CircleDomainRigidity.orientedParameter line 18
  2. theorem OAI.CircleDomainRigidity.contDiff_orientedParameter line 21
  3. theorem OAI.CircleDomainRigidity.orientedCircuit_periodic line 27
  4. theorem OAI.CircleDomainRigidity.abs_circleFormIntegral_oriented line 34
  5. theorem OAI.CircleDomainRigidity.exists_ordered_unit_circuit line 46
  6. theorem OAI.CircleDomainRigidity.exists_ordered_physical_collar line 88