Jordan–Brouwer separation theorem

jordan_brouwer

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. The high-dimensional generalization of the Jordan curve theorem: for d ≥ 2, the complement in ℝᵈ of a topological (d-1)-sphere has exactly two connected components. The hypothesis 2 ≤ d is essential: in dimension d = 1 the (d-1)-sphere is the two-point set {-1, 1}, whose complement in ℝ has three connected components. Mathlib has Metric.sphere, EuclideanSpace, ConnectedComponents, Nat.card, but no Jordan–Brouwer separation theorem, no Alexander duality, no invariance of domain in a form that would discharge it. Stateable with zero new definitions.

Source: L. E. J. Brouwer, *Beweis des Jordanschen Satzes für den n-dimensionalen Raum*, Math. Annalen 71 (1912) (first proof). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover.

Informal solution: Modern proofs use singular homology via Alexander duality: H̃_0(ℝᵈ ∖ Σ) ≅ H̃^{d-1}(Σ), and an embedded (d-1)-sphere Σ has H̃^{d-1}(Σ) ≅ ℤ, giving exactly two components. Brouwer's original proof used direct simplicial-approximation arguments without modern homology.

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

Solved by

Not yet solved.