Zulip Chat Archive

Stream: maths

Topic: Silly function on the reals


view this post on Zulip Chris Hughes (Jul 28 2018 at 18:41):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:42):

that's the Conway base-13 function

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 19:11):

[other functions with this property are available]

view this post on Zulip 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