Zulip Chat Archive

Stream: Is there code for X?

Topic: inequality involving `/2`


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

Scott Morrison (Mar 01 2021 at 06:29):

Ahhh:

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

Scott Morrison (Mar 01 2021 at 06:29):

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

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.

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!

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: Dec 20 2023 at 11:08 UTC