Zulip Chat Archive

Stream: general

Topic: inf_le_inf_left


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 00:56):

both add_le_add_left and mul_le_mul_of_nonneg_left use (a)

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 00:57):

Same with sub_le_sub_left, mul_lt_mul_of_pos_left.

view this post on Zulip Mario Carneiro (May 07 2020 at 01:07):

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

view this post on Zulip Bryan Gin-ge Chen (May 07 2020 at 01:09):

#2109 is similar I guess.

view this post on Zulip 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: May 16 2021 at 05:21 UTC