OAI/Analysis/CircleDomains/Topology/DiskRaySides.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Jordan filling is one of the two actual crosscut components. Consequently its exterior inside the disk is connected as well.

  1. theorem OAI.CircleDomainRigidity.diskRayJordan_subset_complement line 15
  2. theorem OAI.CircleDomainRigidity.diskRay_component_in_or_out line 28
  3. theorem OAI.CircleDomainRigidity.diskRay_exterior_connected line 53