le_or_le

Stream: Is there code for X?

[Johan Commelin]

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

[Bryan Gin-ge Chen]

docs#le_total ?

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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