Connected, but not path-connected space

Stream: Is there code for X?

[Michael Stoll]

I have just been idly wondering (this came up in our Math Support Center, where my wife is working) whether there is a formalization in Lean of the standard fact that the subset of the plane given as
$\qquad M = \{0\} \times [-1,1] \cup \{(x, \sin \frac{1}{x}) : 0 < x \le 1\}$
is connected, but not path-connected?

This is one of the more difficult standard exercises in a first year Analysis course (in Germany). Maybe a more precise question is how to best translate the necessary arguments to Lean, in particular for the "not path-connected" part.

[Patrick Massot]

I would be surprised if we have it. mathlib has very few counter-examples like this

[Eric Wieser]

However, we do have a counterexamples directory where such a result could live

[Michael Stoll]

... but apparently it doesn't.