## Stream: maths

### Topic: is_interval

#### Heather Macbeth (Aug 31 2020 at 20:03):

Asked by @Floris van Doorn on #3991, @Yury G. Kudryashov or @Patrick Massot or @Anatole Dedecker will know:

Do we have a name for the following property?

def is_interval (s : set α) : Prop := ∀ (x y ∈ s) z, x < z → z < y → z ∈ s


I'm not sure about the name is_connected might be another potential name, but that sounds very topological. It is at least the property shared by all intervals.

#### Johan Commelin (Aug 31 2020 at 20:08):

is_preconnected doesn't require nonemptiness.

#### Johan Commelin (Aug 31 2020 at 20:08):

But it is of course not stated in the way you give it.

#### Johan Commelin (Aug 31 2020 at 20:08):

So we would need an iff lemma to connect it to the formula you want

#### Heather Macbeth (Aug 31 2020 at 20:11):

Ah -- and linked to from docs#is_preconnected_interval there is docs#set.ord_connected, which perhaps is better

#### Patrick Massot (Aug 31 2020 at 20:12):

I was really confused because I started to look for this and could only find docs#is_order_connected. I almost had the right name...

#### Floris van Doorn (Aug 31 2020 at 20:12):

Ah ord_connected is basically the same as what I wrote. I think that would be a good condition

oh I'm too slow

#### Heather Macbeth (Aug 31 2020 at 20:13):

Yep, it's perfect.

#### Heather Macbeth (Aug 31 2020 at 20:14):

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

#### Heather Macbeth (Aug 31 2020 at 20:14):

9 I guess, counting the nonexistent Iii.

#### Anatole Dedecker (Aug 31 2020 at 20:14):

Patrick Massot said:

I was really confused because I started to look for this and could only find docs#is_order_connected. I almost had the right name...

Same here I knew it existed but I didn't remember the name

#### Anatole Dedecker (Aug 31 2020 at 20:15):

Heather Macbeth said:

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

I've seen this lemma already I think

#### Floris van Doorn (Aug 31 2020 at 20:18):

Heather Macbeth said:

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

But there are proofs that the 9 intervals (the 9th is called univ :) ) are ord_connected, which is the only direction we need for your application, right?

#### Heather Macbeth (Aug 31 2020 at 20:19):

That's right! But classification theorems are nice, even the trivial ones :)

#### Floris van Doorn (Aug 31 2020 at 20:20):

Agreed. but it's not true in an arbitrary linear order, right? Maybe for a conditionally complete linear order or something?

#### Anatole Dedecker (Aug 31 2020 at 20:21):

https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected.mem_intervals

#### Anatole Dedecker (Aug 31 2020 at 20:22):

But I haven't looked precisely, there might be some subtle difference

#### Heather Macbeth (Aug 31 2020 at 20:24):

Nice! We have Yury to thank it seems, #2943

#### Patrick Massot (Aug 31 2020 at 20:26):

This is a topological result, not purely about order relation.

#### Patrick Massot (Aug 31 2020 at 20:26):

But the general claim is probably wrong.

#### Patrick Massot (Aug 31 2020 at 20:26):

I know I asked Yury to prove this lemma because it was on the undergrad todo list.

#### Heather Macbeth (Aug 31 2020 at 20:28):

Yes, I guess in $(0,1)\cup (2,3)$, the set $(2,3)$ is not an interval

#### Patrick Massot (Aug 31 2020 at 20:31):

Sorry, I don't understand this message.

#### Heather Macbeth (Aug 31 2020 at 20:33):

Did I make a mistake in my counterexample? $]0,1[\cup ]2, 3[$ in French notation.

#### Patrick Massot (Aug 31 2020 at 20:34):

I don't understand the claim, but I should go sleeping (I also haven't forget that I initiated a discussion about fancy composition and didn't find time to come back to it at a time when I can think seriously).

#### Heather Macbeth (Aug 31 2020 at 20:36):

I claimed that if the ordered space is the union of Ioo 0 1 and Ioo 2 3 (taken from the real numbers), and the set s is Ioo 2 3, then s satisfies ord_connected but is not an interval.

#### Heather Macbeth (Aug 31 2020 at 20:36):

But operating on low sleep here too :)

#### Kenny Lau (Aug 31 2020 at 20:37):

as in it isn't Ioo or a friend thereof?

#### Patrick Massot (Aug 31 2020 at 20:38):

Oh, that's sneaky.

#### Patrick Massot (Aug 31 2020 at 20:38):

No, it's not Ioo because 2 and 3 don't exist there.

#### Kenny Lau (Aug 31 2020 at 20:38):

and the point is that it ins't an Ioi either

#### Patrick Massot (Aug 31 2020 at 20:38):

I also had to stare at my screen for 30 seconds to see that.

#### Patrick Massot (Aug 31 2020 at 20:39):

Yes, it's not Ioi either, because of the other piece.

#### Patrick Massot (Aug 31 2020 at 20:40):

And now I'll go and meditate this in my bed.

#### Patrick Massot (Aug 31 2020 at 20:41):

Kids go back to school tomorrow, it's time to resume having a structured life.

#### Anatole Dedecker (Aug 31 2020 at 20:45):

That's a clever counterexample

#### Reid Barton (Aug 31 2020 at 20:59):

in fact, I think it fails in every ordered field other than $\mathbb{R}$

#### Kevin Buzzard (Aug 31 2020 at 21:57):

How about is_convex?

(for a name)

#### Reid Barton (Aug 31 2020 at 22:12):

or if that's too overloaded, perhaps order_convex

#### Heather Macbeth (Aug 31 2020 at 22:49):

But there already is a name, right? docs#set.ord_connected

#### Reid Barton (Aug 31 2020 at 22:50):

Yes but it's too similar to is_order_connected, as Patrick and I found.

#### Heather Macbeth (Aug 31 2020 at 22:54):

I see. Personally I think "convex" should be reserved for objects with addition, though.

#### Adam Topaz (Aug 31 2020 at 22:56):

What about probability measures? They form a convex set :grinning_face_with_smiling_eyes:

#### Reid Barton (Aug 31 2020 at 22:56):

oh right, and the other problem with the name is something ord_connected doesn't have to be connected in the order topology