Zulip Chat Archive

Stream: Is there code for X?

Topic: inequality involving `/2`


view this post on Zulip Scott Morrison (Mar 01 2021 at 06:24):

I am finding this unusually painful. Can anyone point me in the right direction:

import data.real.basic
example (a b : ) : a/2 + b < a  b < a/2 := sorry

view this post on Zulip Scott Morrison (Mar 01 2021 at 06:29):

Ahhh:

example (a b : ) : a/2 + b < a  b < a/2 := by fsplit; { intro, linarith, }

view this post on Zulip Scott Morrison (Mar 01 2021 at 06:29):

I still wouldn't mind seeing a "by hand" proof.

view this post on Zulip Damiano Testa (Mar 01 2021 at 06:45):

Does this count as "by hand"?

example (a b : ) : a/2 + b < a  b < a/2 :=
by rw [ lt_sub_iff_add_lt', sub_half]

Since those are chains of iff's, you may be able to avoid the rw.

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:26):

Scott, I am not really sure that I can help you with using Lean, but I had seen halfs before somewhere else and I guessed that a lemma to move the a / 2 summand to the right would focus on the subafter the fact, so I searched for lt_sub... instead of add_lt....

I do feel silly making these comments to you, but, putting them in writing, helps clear out something in my mind as well!

view this post on Zulip Scott Morrison (Mar 01 2021 at 07:32):

Ah! It was lt_sub_iff_add_lt' that I failed to find. Thank you.


Last updated: May 17 2021 at 16:26 UTC