lt_of_add_lt

Stream: Is there code for X?

[Benjamin Davidson]

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)

[Johan Commelin]

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?

[Benjamin Davidson]

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?

[Benjamin Davidson]

Johan Commelin said:

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

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

[Benjamin Davidson]

Perhaps searching with ℝ is too specific?

[Johan Commelin]

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

[Benjamin Davidson]

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

[Benjamin Davidson]

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

[Benjamin Davidson]

#6171