Zulip Chat Archive

Stream: new members

Topic: km < kn => m < n


view this post on Zulip Li Xuanji (Jun 03 2020 at 15:37):

Does mathlib have this lemma allowing dividing through an inequality?

lemma lt_mul_cancel (n m k : ) (h_k : k > 0) : (k*m < k*n)  (m < n) :=
sorry

I briefly looked through data/nat/lemmas.lean and couldn't find it

view this post on Zulip Shing Tak Lam (Jun 03 2020 at 15:45):

mul_lt_mul_left

library_search finds it btw

import data.nat.basic

lemma lt_mul_cancel (n m k : ) (h_k : k > 0) : (k*m < k*n)  (m < n) :=
(mul_lt_mul_left h_k).1

view this post on Zulip Li Xuanji (Jun 03 2020 at 15:48):

ah thanks!

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:15):

any hope that this one is in mathlib? library_search didn't find it

lemma lt_mul_cancel (n m k : ) (h_k : k > 1) : (k*m + 1 < k*n)  (m < n) :=
begin
  sorry
end

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:16):

if not, would I have to work over \R to prove it?

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:35):

lemma lt_mul_cancel (n m k : ) (h_k : 1 < k) : (k*m + 1 < k*n)  (m < n) :=
begin
  intro h,
  refine lt_of_mul_lt_mul_left _ (show 0  k, by linarith),
    refine lt_trans _ h,
    omega,
end

There's a proof which works over nat

view this post on Zulip Reid Barton (Jun 03 2020 at 16:44):

Is this the statement you want? if km+1<knkm + 1 < kn then km<km+1<knkm < km + 1 < kn

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:53):

@Kevin Buzzard thanks!

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:53):

@Reid Barton I think that implies my statement

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:53):

actually I'm not sure

view this post on Zulip Reid Barton (Jun 03 2020 at 16:54):

I thought maybe you got the statement wrong, because it has a stronger hypothesis than lt_mul_cancel so it immediately reduces to that one.

view this post on Zulip Li Xuanji (Jun 03 2020 at 16:59):

oops, I named both statements lt_mul_cancel

view this post on Zulip Li Xuanji (Jun 03 2020 at 17:00):

but I thought they are different, since the second one relies on the fact that 1/k < 1 for most naturalsk

view this post on Zulip Reid Barton (Jun 03 2020 at 17:13):

But k > 1 isn't actually needed for the second one. So either at least one of us is confused, or the statement is the wrong one.

view this post on Zulip Li Xuanji (Jun 04 2020 at 01:34):

oh yeah I see what you mean


Last updated: May 10 2021 at 00:31 UTC