Zulip Chat Archive

Stream: new members

Topic: converting numbers between ℕ, ℚ and ℝ


Jia Ming Lim (Jul 13 2020 at 19:35):

Hi, I'm Jia Ming. This sounds a little silly but I have no clue how to deduce 0<↑n from 0<(n : ℕ) :( I'm stuck on the Real Numbers Game proving that the rationals are dense in R\mathbb{R}. I've almost got it but what seems like the simplest most obvious thing ever stopped me. It would be super helpful to know where I can learn exactly how Lean handles the conversion of numbers between types.

Kevin Buzzard (Jul 13 2020 at 19:36):

You shouldn't be playing that level, it's not ready :-)

Kevin Buzzard (Jul 13 2020 at 19:36):

But maybe norm_cast will help.

Jia Ming Lim (Jul 13 2020 at 19:37):

Ohhh no wonder, I was wondering why a lot of things seems to be missing

Jia Ming Lim (Jul 13 2020 at 19:37):

Thanks! I'll try that

Kevin Buzzard (Jul 13 2020 at 19:37):

The first 7 levels are ready.

Johan Commelin (Jul 13 2020 at 19:37):

@Jia Ming Lim

It would be super helpful to know where I can learn exactly how Lean handles the conversion of numbers between types.

This is exactly what will be one of the topics in the workshop tomorrow!

Kevin Buzzard (Jul 13 2020 at 19:37):

and "max" is ready: http://wwwf.imperial.ac.uk/~buzzard/xena/max_minigame/

Jia Ming Lim (Jul 13 2020 at 19:38):

Omg yeah I played that, so super fun

Kevin Buzzard (Jul 13 2020 at 19:39):

I'm a bit busy this week, but we'll have an abs minigame soon :-) We'll then get on to limits.

Amos Turchet (Jul 13 2020 at 19:41):

all these new games will kill my research in these next weeks :D

Jia Ming Lim (Jul 13 2020 at 20:39):

YES!!!!! THANK YOU ALL, I DID IT HAHAHAH my proof is super messy but it workssss <3


Last updated: Dec 20 2023 at 11:08 UTC