Silly function on the reals

Stream: maths

[Chris Hughes]

I overheard people talking about this function the other day. Can anyone prove its existence?

[Chris Hughes]

import data.real.basic

lemma silly_function : ∃ f : ℝ → ℝ, ∀ x y a : ℝ, x < y → ∃ z : ℝ, x < z ∧ z < y ∧ f z = a := sorry

[Kenny Lau]

that's the Conway base-13 function

[Kevin Buzzard]

[other functions with this property are available]

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Conway_base_13_function . It's an extreme counterexample to "is the converse of the intermediate value theorem true?"