Two-sided Jordan accessibility from arc non-separation

Proved

JordanCurve.accessibility_from_arc_complement

by Mazecto · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

topology

Assume the planar simple-arc non-separation theorem. For any simple closed curve $J$ whose complement is divided into two disjoint open connected regions $U,V$ , every curve point can be approached from both regions:

J\subseteq\overline U\cap\overline V.

This identifies the local topological deduction that follows the arc-complement result.

Preamble

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Topology.Connected.Basic
import Mathlib.Topology.Bornology.Basic

Formal statement

namespace JordanCurve
theorem accessibility_from_arc_complement
    (hArc : ∀ α : Set.Icc (0 : ℝ) 1 → EuclideanSpace ℝ (Fin 2),
      Continuous α → Function.Injective α →
        IsConnected ((Set.range α)ᶜ))
    (γ : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 →
      EuclideanSpace ℝ (Fin 2))
    (hγ : Continuous γ) (hinj : Function.Injective γ)
    (inside outside : Set (EuclideanSpace ℝ (Fin 2)))
    (hiopen : IsOpen inside) (hoopen : IsOpen outside)
    (hiconn : IsConnected inside) (hoconn : IsConnected outside)
    (hdisj : Disjoint inside outside)
    (hcover : inside ∪ outside = (Set.range γ)ᶜ) :
    Set.range γ ⊆ closure inside ∩ closure outside := by sorry
end JordanCurve

Source

Schoenflies/JordanClosed.lean, Jordan theorem derived from arc complement, https://github.com/alonamaloh/schoenflies-lean/blob/main/Schoenflies/JordanClosed.lean.

View graph