Zulip Chat Archive
Stream: maths
Topic: betweenness
Chris Hughes (May 29 2019 at 14:02):
Do we have a concept of betweenness in mathlib for orders? i.e a is between x and y iff min x y ≤ a ∧ a ≤ max x y
Chris Hughes (May 29 2019 at 14:03):
I want it for partial orders though.
Mario Carneiro (May 29 2019 at 14:18):
It's not clear what the analogue is... how did this come up?
Mario Carneiro (May 29 2019 at 14:18):
Usually you know which of x or y is bigger and then x <= a <= y does mostly what you want
Mario Carneiro (May 29 2019 at 14:20):
Perhaps x ⊓ y ≤ a ≤ x ⊔ y?
Last updated: Dec 20 2023 at 11:08 UTC