Zulip Chat Archive
Stream: Is there code for X?
Topic: Smallest integer greater than a real
shortc1rcuit (Jul 19 2023 at 20:30):
How would I write this in lean?
"Let p be the smallest integer such that p > qa. Then p - 1 <= qa."
qa is a real number.
Eric Wieser (Jul 19 2023 at 20:32):
shortc1rcuit (Jul 19 2023 at 20:36):
Ah ok. Thanks
shortc1rcuit (Jul 19 2023 at 21:46):
Actually this doesn't work as that would get me "p >= qa. Then p - 1 < qa" which has the incorrect inequalities.
Eric Wieser (Jul 19 2023 at 21:50):
Ah, then you want Int.floor r + 1
Eric Wieser (Jul 19 2023 at 21:50):
Sorry, I gave you the smallest integer greater than or equal to a real
shortc1rcuit (Jul 19 2023 at 21:57):
Cool
Interestingly enough the proof I'm following has me first prove that there exists an greater than qa. But using your method means I don't have to use that step.
Last updated: Dec 20 2023 at 11:08 UTC