ConnectedCoreExhaustion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Connected retained-core exhaustions

Compact exhaustion and paths in an open plane domain give nested connected open cores with compact closure in that domain. Adjoining one fixed exterior then gives the cofinite cores required by normalized model compactness.

theorem OAI.CircleDomainRigidity.exists_connected_plane_exhaustion line 22

theorem OAI.CircleDomainRigidity.exists_cofinite_connected_plane_exhaustion line 72

Source documentation

The cofinite cores retain a full fixed exterior, while the closure of every core stays in the original domain.

theorem exists_cofinite_connected_plane_exhaustion
    {G : Set ℂ} (hG : IsOpen G) (hconn : IsConnected G)
    {R : ℝ} (hR : 0 < R) (hext : {z : ℂ | R ≤ ‖z‖} ⊆ G) :
    ∃ D : ℕ → Set ℂ,
      (∀ n, IsOpen (D n)) ∧ (∀ n, IsConnected (D n)) ∧ Monotone D ∧
      (∀ n, closure (D n) ⊆ G) ∧ (⋃ n, D n) = G ∧
      {z : ℂ | 2 * R ≤ ‖z‖} ⊆ D 0 := by
…