SphereNeighborhoods.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Connected-complement neighborhoods on the concrete sphere

Finite points use ordinary round disks. Infinity uses complements of closed round disks. Thus every open sphere neighborhood contains the closure of an open neighborhood with connected complement, as needed for contour filling.

theorem OAI.CircleDomainRigidity.infty_mem_closure_image_of_unbounded line 18
theorem OAI.CircleDomainRigidity.isConnected_complex_exterior_closedBall_center line 28
theorem OAI.CircleDomainRigidity.unbounded_complex_exterior line 42
theorem OAI.CircleDomainRigidity.isConnected_sphere_exterior_closedBall line 49
theorem OAI.CircleDomainRigidity.isConnected_sphere_exterior_ball line 67
theorem OAI.CircleDomainRigidity.exists_sphere_neighborhood_connected_compl line 90
Source documentation
A concrete sphere basis with compact containment and connected complements. At finite points the neighborhoods are physical round disks; at infinity they are exteriors of physical closed round disks.
```
theorem exists_sphere_neighborhood_connected_compl
    {W : Set Sphere} (hW : IsOpen W) {x : Sphere} (hx : x ∈ W) :
    ∃ V : Set Sphere, IsOpen V ∧ x ∈ V ∧ closure V ⊆ W ∧ IsConnected Vᶜ := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere