OAI/Analysis/CircleDomains/Topology/JordanIntersectionConnectivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Connectivity on the inside of a retained Jordan boundary

A radial clamp onto a slightly smaller disk fixes any prescribed pair of interior points and maps the whole domain into its intersection with the disk. The inner circle stays in the domain by compactness of the retained boundary. This proves the connectedness needed to track source and image sides under refinement.

  1. def OAI.CircleDomainRigidity.radialClamp line 23
  2. theorem OAI.CircleDomainRigidity.continuous_radialClamp line 25
  3. theorem OAI.CircleDomainRigidity.radialClamp_eq_self line 30
  4. theorem OAI.CircleDomainRigidity.norm_radialClamp_of_le line 34
  5. theorem OAI.CircleDomainRigidity.inner_circle_subset_of_retained_boundary line 40
  6. theorem OAI.CircleDomainRigidity.isPreconnected_inter_unitDisk line 60
  7. theorem OAI.CircleDomainRigidity.isPreconnected_inter_jordanInterior line 88