Zulip Chat Archive

Stream: general

Topic: inf_le_inf_left

Yury G. Kudryashov (May 07 2020 at 00:54):

I found out that inf_le_inf_left and sup_le_sup_left have different ideas about left/right. Which one do you prefer:
(a) left is a op b ≤ a op c;
(b) left is a op c ≤ b op c?

Yury G. Kudryashov (May 07 2020 at 00:56):

both add_le_add_left and mul_le_mul_of_nonneg_left use (a)

Yury G. Kudryashov (May 07 2020 at 00:57):

Same with sub_le_sub_left, mul_lt_mul_of_pos_left.

Mario Carneiro (May 07 2020 at 01:07):

I would suggest taking a tally of existing mathlib theorems to find consensus, which suggests (a)

Bryan Gin-ge Chen (May 07 2020 at 01:09):

#2109 is similar I guess.

Kenny Lau (May 07 2020 at 01:10):

inconsistencies like this are why I just try both variants (left and right) whenever I need to use such a theorem

Last updated: Aug 03 2023 at 10:10 UTC