The "topologist's sine curve" is connected but not path-connected

We give an example of a closed subset T of ℝ × ℝ which is connected but not path-connected: the closure of the set { (x, sin x⁻¹) | x ∈ Ioi 0 }.

Main results

• TopologistsSineCurve.isConnected_T: the set T is connected.
• TopologistsSineCurve.not_isPathConnected_T: the set T is not path-connected.

This formalization is part of the UniDistance Switzerland bachelor thesis of Daniele Bolla. A similar result has also been independently formalized by Vlad Tsyrklevich (https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/golf.20request.3A.20Topologist's.20sine.20curve).

def TopologistsSineCurve.S : Set (ℝ × ℝ)

The topologist's sine curve, i.e. the graph of y = sin (x⁻¹) for 0 < x.

Equations

• TopologistsSineCurve.S = (fun (x : ℝ) => (x, Real.sin x⁻¹)) '' Set.Ioi 0

def TopologistsSineCurve.Z : Set (ℝ × ℝ)

The vertical line segment { (0, y) | -1 ≤ y ≤ 1 }, which is the set of limit points of S not contained in S itself.

Equations

• TopologistsSineCurve.Z = (fun (y : ℝ) => (0, y)) '' Set.Icc (-1) 1

def TopologistsSineCurve.T : Set (ℝ × ℝ)

The union of S and Z (which we will show is the closure of S).

Equations

• TopologistsSineCurve.T = TopologistsSineCurve.S ∪ TopologistsSineCurve.Z

noncomputable def TopologistsSineCurve.xSeq (y : ℝ) (k : ℕ) : ℝ

A sequence of x-values tending to 0 at which the sine curve has a given y-coordinate.

Equations

• TopologistsSineCurve.xSeq y k = 1 / (Real.arcsin y + (↑k + 1) * (2 * Real.pi))

theorem TopologistsSineCurve.xSeq_pos (y : ℝ) (k : ℕ) : 0 < xSeq y k

theorem TopologistsSineCurve.sin_inv_xSeq {y : ℝ} (hy : y ∈ Set.Icc (-1) 1) (k : ℕ) : Real.sin (xSeq y k)⁻¹ = y

theorem TopologistsSineCurve.xSeq_tendsto (y : ℝ) : Filter.Tendsto (xSeq y) Filter.atTop (nhds 0)

T is closed

theorem TopologistsSineCurve.closure_S : closure S = T

The closure of the topologist's sine curve S is the set T.

theorem TopologistsSineCurve.isClosed_T : IsClosed T

T is connected

theorem TopologistsSineCurve.isConnected_T : IsConnected T

T is connected, being the closure of the set S (which is obviously connected since it is a continuous image of the positive real line).

T is not path-connected

theorem TopologistsSineCurve.zero_mem_T : (0, 0) ∈ T

noncomputable def TopologistsSineCurve.w : ℝ × ℝ

A point in the body of the topologist's sine curve.

Equations

• TopologistsSineCurve.w = (1, Real.sin 1⁻¹)

theorem TopologistsSineCurve.w_mem_T : w ∈ T

theorem TopologistsSineCurve.exists_mem_Ioc_of_y {y : ℝ} (hy : y ∈ Set.Icc (-1) 1) {a : ℝ} (ha : 0 < a) : ∃ x ∈ Set.Ioc 0 a, Real.sin x⁻¹ = y

For any 0 < a and any y ∈ Icc (-1) 1, we can find x ∈ Ioc a 0 with sin x⁻¹ = y.

theorem TopologistsSineCurve.not_isPathConnected_T : ¬IsPathConnected T

The set T is not path-connected.