JordanExteriors.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The common exterior of finitely many disjoint Jordan disks

Removing finitely many disjoint closed Jordan disks leaves a preconnected set. We first prove the closed-complement version by extending any separation across disks according to which side contains their connected boundaries. Small enlargements of the disks then give the open-complement version. These are proved topology lemmas, not additional published inputs.

theorem OAI.CircleDomainRigidity.isPreconnected_compl_finite_open_disks line 24

Source documentation

Fill connected boundary components into either side of a hypothetical separation. Finiteness makes both enlarged sides closed.

theorem isPreconnected_compl_finite_open_disks
    {X I : Type*} [TopologicalSpace X] [PreconnectedSpace X] [Finite I]
    (U : I → Set X) (hU : ∀ i, IsOpen (U i))
    (hfront : ∀ i, IsPreconnected (frontier (U i)))
    (hdisj : Pairwise (Disjoint on fun i => closure (U i))) :
    IsPreconnected (⋃ i, U i)ᶜ := by
…

theorem OAI.CircleDomainRigidity.exists_disjoint_jordan_enlargements line 108

Source documentation

Enlarge finitely many disjoint closed Jordan disks within prescribed open neighborhoods, keeping their closures disjoint.

theorem exists_disjoint_jordan_enlargements
    {I : Type*} [Finite I] (H : I → ℂ ≃ₜ ℂ)
    (hdisj : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    (O : I → Set ℂ) (hO : ∀ i, IsOpen (O i))
    (hsub : ∀ i, closure (jordanInterior (H i)) ⊆ O i) :
    ∃ r : I → ℝ, (∀ i, 1 < r i) ∧
      (∀ i, H i '' closedBall (0 : ℂ) (r i) ⊆ O i) ∧
      Pairwise (Disjoint on fun i => H i '' closedBall (0 : ℂ) (r i)) := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.isPreconnected_exterior_finite_jordanInteriors line 147
Source documentation
Any two points outside the closed disks remain in the connected complement of a sufficiently small simultaneous enlargement.
```
theorem isPreconnected_exterior_finite_jordanInteriors
    {I : Type*} [Finite I] (H : I → ℂ ≃ₜ ℂ)
    (hdisj : Pairwise (Disjoint on fun i => closure (jordanInterior (H i)))) :
    IsPreconnected (⋃ i, closure (jordanInterior (H i)))ᶜ := by
…
```
Mentions: OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.open_subset_finite_jordan_fills_of_frontier_subset line 197

Source documentation

A bounded open set cannot occupy the common exterior when its boundary is covered by finitely many disjoint closed Jordan disks.

theorem open_subset_finite_jordan_fills_of_frontier_subset
    {I : Type*} [Finite I] (H : I → ℂ ≃ₜ ℂ)
    (hdisj : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    {U : Set ℂ} (hU : IsOpen U) (hUbdd : Bornology.IsBounded U)
    (hfront : frontier U ⊆ ⋃ i, closure (jordanInterior (H i))) :
    U ⊆ ⋃ i, closure (jordanInterior (H i)) := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.open_subset_finite_jordanInteriors_of_frontier_subset line 229

Source documentation

If the selected contours are themselves boundary curves of the open set, coverage by closed fills is coverage by their interiors.

theorem open_subset_finite_jordanInteriors_of_frontier_subset
    {I : Type*} [Finite I] (H : I → ℂ ≃ₜ ℂ)
    (hdisj : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    {U : Set ℂ} (hU : IsOpen U) (hUbdd : Bornology.IsBounded U)
    (hcover : frontier U ⊆ ⋃ i, closure (jordanInterior (H i)))
    (hselected : ∀ i, frontier (jordanInterior (H i)) ⊆ frontier U) :
    U ⊆ ⋃ i, jordanInterior (H i) := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior