Zulip Chat Archive

Stream: new members

Topic: 0 < 0.1


view this post on Zulip Iocta (Jul 04 2020 at 20:10):

example : 0 < 0.1:= sorry

How to prove this?

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 20:11):

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

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:11):

what type are you talking about?

view this post on Zulip Reid Barton (Jul 04 2020 at 20:11):

it can be true, depending on the proof!

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

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:11):

aha so it can

view this post on Zulip Iocta (Jul 04 2020 at 20:11):

ah, if I : real them, norm_num works

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:11):

if you use theorem then it won't do that

view this post on Zulip 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: May 14 2021 at 12:18 UTC