OAI/Analysis/CircleDomains/Topology/QuotientDiskTopology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Topology of projected physical disks

Physical Jordan disks with boundary in the original domain have saturated interiors and saturated closures. Their images are open with connected complements, and disjoint physical closed disks give disjoint quotient closed disks. These properties allow finite dust covers to be used in the descending grid construction without postulating a disk-selection lemma.

  1. theorem OAI.CircleDomainRigidity.isConnected_sphere_compl_jordanInterior line 20
  2. theorem OAI.CircleDomainRigidity.preimage_image_closure_of_singleton_boundary_fibers line 30
  3. theorem OAI.CircleDomainRigidity.preimage_image_closed_jordanInterior_of_component_collapse line 50
  4. theorem OAI.CircleDomainRigidity.image_compl_of_saturated line 68
  5. theorem OAI.CircleDomainRigidity.isConnected_compl_image_jordanInterior_of_component_collapse line 81
  6. theorem OAI.CircleDomainRigidity.disjoint_images_of_saturated line 93

    Source documentation

    Disjointness descends for saturated physical closed fills.

    theorem disjoint_images_of_saturated {X Y : Type*} (π : X → Y) {A B : Set X}
    (hsat : π ⁻¹' (π '' A) = A) (hd : Disjoint A B) :
    Disjoint (π '' A) (π '' B) := by
…
  7. theorem OAI.CircleDomainRigidity.physical_preimage_image_jordanInterior line 104
  8. theorem OAI.CircleDomainRigidity.closure_image_jordanInterior line 116
  9. theorem OAI.CircleDomainRigidity.infty_notMem_closure_image_jordanInterior line 123