## Stream: maths

### Topic: Silly function on the reals

#### Chris Hughes (Jul 28 2018 at 18:41):

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

#### Chris Hughes (Jul 28 2018 at 18:42):

import data.real.basic

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


#### Kenny Lau (Jul 28 2018 at 18:42):

that's the Conway base-13 function

#### Kevin Buzzard (Jul 28 2018 at 19:11):

[other functions with this property are available]

#### Kevin Buzzard (Jul 28 2018 at 19:13):

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

Last updated: May 18 2021 at 07:19 UTC