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