theorem inconsistency in mathlib?

Stream: new members

[ccn]

Hello, I was looking for a theorem in mathlib and I found these ones:

image.png

https://leanprover-community.github.io/mathlib_docs/init/algebra/order.html#gt_of_gt_of_ge

It looks like the first two used a curried version and the second two (to do with gt) seem to use assumptions, should they both be curried or is it like that for a reason?

[Huỳnh Trần Khanh]

there is no inconsistency here :joy: different ways of doing the same thing, but the type signature is still the same

it's just that the type signature is displayed differently lol

[Yakov Pechersky]

In mathlib3, we try not to use ge or gt. They are different symbols and this means that rewriting something that has a ge with something that expects an le to be written might fail. Again, in lean3. So these helper lemmas exist as an escape hatch in the cases where you still have a ge.

[Kyle Miller]

I'm not sure exactly why the first two theorems are written using match notation, since they could equally well have been written as

@[trans] lemma lt_of_lt_of_le' {a b c : α} (hab : a < b) (hbc : b ≤ c) : a < c :=
let ⟨hab, hba⟩ := le_not_le_of_lt hab in
lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca)

@[trans] lemma lt_of_le_of_lt' {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c :=
let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in
lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab)

The gt lemmas, if you wanted them to show up in the docs with anonymous arguments, could have been written like so:

@[trans] lemma gt_of_gt_of_ge' {a b c : α} : a > b → b ≥ c → a > c :=
flip lt_of_le_of_lt

@[trans] lemma gt_of_ge_of_gt' {a b c : α} : a ≥ b → b > c → a > c :=
flip lt_of_lt_of_le

(I'm using primes so my version doesn't conflict with the existing one.)