Smooth Schoenflies theorem for $S^1\subset S^2$

Open

SmoothSchoenflies.smooth_schoenflies_dim_two

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^1\to S^2$ be a smooth embedding and $x\in S^2\setminus f(S^1)$ , with $C_x$ the component of $S^2\setminus f(S^1)$ containing $x$ . Then

\overline{C_x}\ \text{is diffeomorphic to}\ D^2.

This is the case $n=1$ of the statement that every smooth $S^n\subset S^{n+1}$ is unknotted.

Formalization Note 'Diffeomorphic to $D^2$ ' is IsSmoothClosedBallIn 1: the image of the closed unit disc under a $C^\infty$ map $\mathbb R^2\to S^2$ injective with injective differential on the disc.

Preamble

import Mathlib
import Definitions.Def_SmoothSchoenflies_basic

open Manifold Metric

Formal statement

namespace SmoothSchoenflies

theorem smooth_schoenflies_dim_two (f : Sph 1 → Sph 2) (hf : IsSmoothEmbeddingSph 1 f)
    (x : Sph 2) (hx : x ∉ Set.range f) :
    IsSmoothClosedBallIn 1 (closure (connectedComponentIn (Set.range f)ᶜ x)) := 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; 'all embeddings of S^n in S^{n+1} are unknotted (bound manifolds diffeomorphic to D^{n+1}) provided n ≠ 3. For n = 1 this is due to Schoenflies.'

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

Smooth Schoenflies theorem for S1⊂S2S^1\subset S^2S1⊂S2

Smooth Schoenflies theorem for $S^1\subset S^2$