Jordan curve theorem

Proved

JordanCurve.jordan_curve_theorem

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

geometrytopology

Let $\gamma:S^1\to\mathbb R^2$ be a continuous injective map, and let $J=\gamma(S^1)$ be its simple closed curve. Then the complement has exactly two connected components: a bounded interior $U$ and an unbounded exterior $V$ . Both are open, they are disjoint, and their common boundary is precisely the curve:

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

In the formal statement, connectedness and the disjoint open partition ensure that these are the two connected components, rather than merely connected subsets.

Preamble

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

Formal statement

namespace JordanCurve

theorem jordan_curve_theorem
    (γ : 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 γ)ᶜ ∧
      frontier inside = Set.range γ ∧
      frontier outside = Set.range γ := by sorry

end JordanCurve

Source

The classical Jordan curve theorem; compare A Proof of the Jordan Curve Theorem, https://doi.org/10.4236/ns.2019.1112037, statement of the Jordan Curve Theorem.

View graph