Jordan curve theorem

jordan_curve

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. Every continuous injection r : S¹ → ℝ² has a complement with exactly two connected components. Mathlib has Metric.sphere, EuclideanSpace, ConnectedComponents, and Nat.card, but no Jordan curve theorem (`grep -ri 'jordan curve' Mathlib/`: no hits), no winding numbers / invariance of domain in a form that would discharge it. Stateable with zero new definitions.

Source: C. Jordan, *Cours d'analyse* (1887, 2nd ed.; first statement and a famously gap-laden proof). The first rigorous proof is by O. Veblen, *Theory on plane curves in non-metrical analysis situs*, Trans. AMS 6 (1905). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Formalized in Mizar (Korniłowicz et al., 2005) and HOL Light (Hales, 2007); not in Lean or Coq mathlib-equivalents.

Informal solution: Modern proofs use either singular homology of the complement (Alexander duality H̃_0(ℝ² ∖ C) ≅ H̃¹(S¹) = ℤ giving exactly two components) or planar combinatorics (approximate by polygonal Jordan curves, use winding-number parity to define inside/outside, transfer to the continuous curve via uniform convergence).

theorem declaration uses `sorry`jordan_curve (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
    (_hcont : Continuous r) (_hinj : Function.Injective r) :
    Nat.card
        (ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin 2)))) =
      2 := byr:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ Nat.card (ConnectedComponents ↑(Set.range r)ᶜ) = 2
  sorryAll goals completed! 🐙

Solved by

Not yet solved.