Zulip Chat Archive

Stream: Is there code for X?

Topic: lt_of_add_lt


view this post on Zulip Benjamin Davidson (Feb 11 2021 at 03:47):

Does the following exist in mathlib?

import analysis.special_functions.trigonometric

example (a b c : ) (h : a + b < c) (hle : 0  b) : a < c := by linarith

As you can see, this can be proven easily by linarith, but I was surprised that I couldn't find an exact statement.

(The import is random)

view this post on Zulip Johan Commelin (Feb 11 2021 at 05:45):

How many variations are there on this lemma? I guess it makes sense to add these, but then we also need things like

example (a b c : ) (h : a < b + c) (hle : b  0) : a < c := _

And also variants where h is a \le and hle becomes hlt.
I guess mathlib already has the variant where everything is \le, right?

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 05:49):

For that matter, I can't find

example (a b c d : ) (h : a + b < c) (hle : d  b) : a + d < c := by linarith

either...surely this must exist in the library?

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 05:51):

Johan Commelin said:

I guess mathlib already has the variant where everything is \le, right?

No, I couldn't find the le variant either.

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 05:51):

Perhaps searching with is too specific?

view this post on Zulip Johan Commelin (Feb 11 2021 at 05:54):

Ooh, right, this is probably a statement about linearly ordered rings

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 06:01):

I just tried a library_search with a, b, and c as members of a linearly ordered ring and got a deterministic timeout :(

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 06:06):

I don't mind adding these but I'd be pretty surprised if none of the variants already exist.

view this post on Zulip Benjamin Davidson (Feb 11 2021 at 08:21):

#6171


Last updated: May 07 2021 at 21:10 UTC