Schoenflies theorem

schoenflies

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². This is the faithful encoding of Knill's prose statement 'each complementary region is homeomorphic to the open disk' — which as literally written is false for the unbounded region (homeomorphic to ℝ² ∖ closedBall 0 1, fundamental group ℤ, not simply connected). The strong form implies the bounded region is homeomorphic to the open disk. Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but no Schoenflies theorem (`grep -ri 'schoenflies' Mathlib/`: no hits), no Jordan curve theorem, no invariance-of-domain machinery in a form that would discharge it. Stateable with zero new definitions.

Source: A. M. Schoenflies, *Beiträge zur Theorie der Punktmengen III*, Math. Annalen 62 (1906) (first proof, with gaps); rigorous proofs by L. Antoine (1921), L. E. J. Brouwer (1909–10). 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: Classical proof: (i) the Jordan curve theorem gives the inside and outside regions; (ii) Riemann mapping for the bounded inside extends to a homeomorphism of the closed disk by Carathéodory's theorem on prime ends; (iii) a parallel construction handles the outside; (iv) the two homeomorphisms patch along the curve to a homeomorphism of ℝ².

theorem declaration uses `sorry`schoenflies (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
    (_hcont : Continuous r) (_hinj : Function.Injective r) :
    ∃ h : EuclideanSpace ℝ (Fin 2) ≃ₜ EuclideanSpace ℝ (Fin 2),
      h '' Set.range r = Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := byr:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ ∃ h, ⇑h '' Set.range r = Metric.sphere 0 1
  sorryAll goals completed! 🐙

Solved by

Not yet solved.