Zulip Chat Archive

Stream: Is there code for X?

Topic: le_or_le


view this post on Zulip Johan Commelin (Mar 04 2021 at 05:53):

Does it make sense to add this to mathlib? (I couldn't find it.)
I often find myself wanting to case on this, and invoking wlog every time is somewhat slow.

lemma le_or_le {α : Type*} [linear_order α] (a b : α) :
  a  b  b  a :=
(le_or_lt a b).imp id le_of_lt

view this post on Zulip Bryan Gin-ge Chen (Mar 04 2021 at 05:54):

docs#le_total ?

view this post on Zulip Johan Commelin (Mar 04 2021 at 06:01):

Aah, the wonders of a predictable naming convention :rofl:

view this post on Zulip Kevin Buzzard (Mar 04 2021 at 07:19):

lt_irrefl is another one which takes some getting used to -- I would always look for not_lt_self.

view this post on Zulip Mario Carneiro (Mar 04 2021 at 07:22):

I think we already have le_or_ge, so I don't think it would be a bad idea to have le_or_le as an alias for le_total

view this post on Zulip Patrick Massot (Mar 04 2021 at 07:50):

I agree we could have aliases for both le_total and lt_irrefl.

view this post on Zulip Yury G. Kudryashov (Mar 04 2021 at 07:55):

We also have an alias docs#has_lt.lt.false


Last updated: May 17 2021 at 16:26 UTC