Zulip Chat Archive

Stream: new members

Topic: 0 < 0.1


Iocta (Jul 04 2020 at 20:10):

example : 0 < 0.1:= sorry

How to prove this?

Kevin Buzzard (Jul 04 2020 at 20:11):

I doubt it's true. They're probably both naturals and both 0

Mario Carneiro (Jul 04 2020 at 20:11):

what type are you talking about?

Reid Barton (Jul 04 2020 at 20:11):

it can be true, depending on the proof!

Kevin Buzzard (Jul 04 2020 at 20:11):

You need to explicitly say which 0 you're talking about, otherwise Lean will assume it's a natural

Mario Carneiro (Jul 04 2020 at 20:11):

aha so it can

Iocta (Jul 04 2020 at 20:11):

ah, if I : real them, norm_num works

Mario Carneiro (Jul 04 2020 at 20:11):

if you use theorem then it won't do that

Jason Orendorff (Jul 04 2020 at 22:06):

oh, 0.1 being interpreted as a natural number seems unfortunate, but I can see why


Last updated: Dec 20 2023 at 11:08 UTC