Jordan–Brouwer separation for smooth $S^n\subset S^{n+1}$

Open

SmoothSchoenflies.jordan_brouwer_separation

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

4-manifoldsdifferential-topologyschoenfliestopology

Let $S^n=\{x\in\mathbb R^{n+1}:\|x\|=1\}$ be the unit sphere with its standard smooth structure and $D^{n+1}=\{x\in\mathbb R^{n+1}:\|x\|\le 1\}$ the closed unit ball. Let $f:S^n\to S^{n+1}$ be a smooth embedding (a $C^\infty$ injective immersion) with image $M=f(S^n)$ . Then $S^{n+1}\setminus M$ has exactly two connected components $U$ and $V$ , and $M$ is the frontier of each:

\partial U=\partial V=M.

This is the separation statement the Schoenflies problem is built on: the two closures $\overline U,\overline V$ are the compact manifolds whose diffeomorphism type the problem asks about.

Formalization Note Components are connectedComponentIn (Set.range f)ᶜ x; the statement asserts two points $x,y\notin M$ with distinct components, every point of the complement lies in one of these two components, and the frontier of each component equals $M$ .

Preamble

import Mathlib
import Definitions.Def_SmoothSchoenflies_basic

open Manifold Metric

Formal statement

namespace SmoothSchoenflies

theorem jordan_brouwer_separation (n : ℕ) (f : Sph n → Sph (n + 1))
    (hf : IsSmoothEmbeddingSph n f) :
    ∃ x y : Sph (n + 1), x ∉ Set.range f ∧ y ∉ Set.range f ∧
      connectedComponentIn (Set.range f)ᶜ x ≠ connectedComponentIn (Set.range f)ᶜ y ∧
      (∀ z ∉ Set.range f,
        connectedComponentIn (Set.range f)ᶜ z = connectedComponentIn (Set.range f)ᶜ x ∨
        connectedComponentIn (Set.range f)ᶜ z = connectedComponentIn (Set.range f)ᶜ y) ∧
      frontier (connectedComponentIn (Set.range f)ᶜ x) = Set.range f ∧
      frontier (connectedComponentIn (Set.range f)ᶜ y) = Set.range f := by sorry

end SmoothSchoenflies

Source

Open Problem Garden, 'Smooth 4-dimensional Schoenflies problem' (posted by rybu, Nov 6 2009), https://www.openproblemgarden.org/op/smooth_4_dimensional_schoenflies_problem; 'By the Jordan-Brouwer separation theorem, M separates S^4 into the union of two compact connected 4-manifolds which share M as a common boundary' (stated there for n = 3; formalized for all n).

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Jordan–Brouwer separation for smooth Sn⊂Sn+1S^n\subset S^{n+1}Sn⊂Sn+1

Jordan–Brouwer separation for smooth $S^n\subset S^{n+1}$