Every Jordan curve point borders both regions

Proved

JordanCurve.simple_closed_curve_two_sided_accessibility

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

topology

Let $J$ be a continuous injective image of the unit circle. Suppose $U$ and $V$ are disjoint open connected sets whose union is the complement of $J$ . Every point of the curve lies in both closures:

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

This is the local two-sidedness part of the Jordan curve theorem.

Preamble

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

Formal statement

namespace JordanCurve
theorem simple_closed_curve_two_sided_accessibility
    (γ : 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

Jordan curve theorem, common-boundary assertion; see A Proof of the Jordan Curve Theorem, https://doi.org/10.4236/ns.2019.1112037.

View graph