OAI/Analysis/CircleDomains/Topology/BoundaryClosingArc.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A positively parametrized boundary arc closes a disk crosscut to a simple loop. The resulting circle uses only the existing Schoenflies input.

  1. theorem OAI.CircleDomainRigidity.standardCirclePoint_zero line 16
  2. theorem OAI.CircleDomainRigidity.boundary_angle_pos line 19
  3. theorem OAI.CircleDomainRigidity.boundary_arc_parameter_mem line 32
  4. def OAI.CircleDomainRigidity.boundaryClosingArc line 38
  5. theorem OAI.CircleDomainRigidity.boundaryClosingArc_norm line 53
  6. theorem OAI.CircleDomainRigidity.boundaryClosingArc_injective line 56
  7. theorem OAI.CircleDomainRigidity.crosscut_boundary_intersections line 68
  8. theorem OAI.CircleDomainRigidity.exists_schoenflies_of_disk_crosscut line 86