OAI/Analysis/CircleDomains/Topology/DiskRayJordan.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual compactified lifted ray bounds a Jordan disk after closing along the positive boundary arc. Its entire filling stays in the unit disk.

  1. def OAI.CircleDomainRigidity.diskRayCrosscut line 16
  2. def OAI.CircleDomainRigidity.diskRayLoop line 23
  3. theorem OAI.CircleDomainRigidity.diskRayLoop_injective_before_end line 28
  4. theorem OAI.CircleDomainRigidity.exists_diskRayJordan line 37
  5. theorem OAI.CircleDomainRigidity.diskRayCrosscut_norm_le line 58
  6. theorem OAI.CircleDomainRigidity.jordan_fill_subset_closed_unitDisk line 68
  7. theorem OAI.CircleDomainRigidity.diskRayJordan_filling_subset line 82