Jordan separation into two regions

Proved

JordanCurve.simple_closed_curve_two_regions

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

topology

A continuous injective image $J$ of the unit circle in the plane has a complement partitioned into two disjoint nonempty open connected regions: one bounded and the other unbounded. Thus

\mathbb R^2\setminus J=U\sqcup V.

These are exactly the two connected components of the complement.

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_regions
    (γ : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 →
      EuclideanSpace ℝ (Fin 2))
    (hγ : Continuous γ) (hinj : Function.Injective γ) :
    ∃ inside outside : Set (EuclideanSpace ℝ (Fin 2)),
      IsOpen inside ∧ IsOpen outside ∧
      IsConnected inside ∧ IsConnected outside ∧
      Bornology.IsBounded inside ∧ ¬ Bornology.IsBounded outside ∧
      Disjoint inside outside ∧
      inside ∪ outside = (Set.range γ)ᶜ := by sorry
end JordanCurve

Source

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

View graph