OAI/Analysis/CircleDomains/Topology/RetainedJordanSides.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A retained Jordan curve separates the two sides of an open connected sphere domain. This applies to the actual finite models without extending the model map across any terminal disk.

  1. theorem OAI.CircleDomainRigidity.isPreconnected_finite_part line 16
  2. theorem OAI.CircleDomainRigidity.isPreconnected_sphere_inter_jordan line 32
  3. theorem OAI.CircleDomainRigidity.inversion_preimage_unitDisk line 43
  4. theorem OAI.CircleDomainRigidity.isPreconnected_sphere_inter_jordan_exterior line 61
  5. theorem OAI.CircleDomainRigidity.open_image_retained_jordan_side_eq line 100