Zulip Chat Archive

Stream: new members

Topic: inequality following from a stronger inequality

view this post on Zulip Damiano Testa (Feb 11 2021 at 04:41):

Dear All,

I use the lemma below to shorten a proof, as is usually the case with lemmas! :wink:

Since I would like the final lemma to go into mathlib, I would like the lemma below to also go. Should this lemma go to some general file (feel free to suggest which!) or should it stay close to the intended application?

Here is a wordy description of the lemma: to prove that the inequality 1 ≤ a * b holds, it suffices to prove

  • the inequality 1 ≤ a; and
  • if 1 < b, then to provide a c ≤ b satisfying 1 ≤ a * c.
    This lemma is mostly useful if c already appears in the context, especially in situations when the terms a and b are complicated.
import algebra.ordered_ring

lemma one_le_mul_of_le_and_of_lt {R : Type*} [linear_ordered_semiring R] {a b : R} (c : R)
  (ha   : 1  a)
  (key  : b < 1  1  a * c  c  b) :
  1  a * b :=
  by_cases A : b < 1,
  { exact (key A).1.trans ((mul_le_mul_left (zero_lt_one.trans_le ha)).mpr (key A).2) },
  { rw  mul_one (1 : R),
    exact mul_le_mul ha (not_lt.mp A) zero_le_one (zero_le_one.trans ha) }

view this post on Zulip Floris van Doorn (Feb 11 2021 at 04:57):

I see no value having this lemma in a general file. This lemma will probably not come up again in this exact form, and even if it does, it is unlikely that the user that wants this lemma will find it.

If you use this in only one theorem, I would not even separate this out as a separate lemma, but just prove it as a have, like this.

view this post on Zulip Damiano Testa (Feb 11 2021 at 05:02):

Floris, thank you so much, also for the commented pointer!

Last updated: May 11 2021 at 23:11 UTC