open interval

Stream: Is there code for X?

[ZHAO Jinxiang]

Is there any definition for open interval?
I want to descript a set of real is set.Ioo or set.Iio or set.Ioi.

[Yaël Dillies]

Do you want an order interval or a geometry interval?

[ZHAO Jinxiang]

What's the difference? I'm learning the topology chapter 1 now.

[Yaël Dillies]

One is about preorders, the other is about vector spaces.

[ZHAO Jinxiang]

Maybe preorder

[Yaël Dillies]

Then docs#set.Ioo

[ZHAO Jinxiang]

But I need set.Ioo or set.Iio or set.Ioi

[Yaël Dillies]

Then Ioo in docs#ereal is an option.

[Yaël Dillies]

Otherwise I have #14807 open to add the type of intervals.

[ZHAO Jinxiang]

This is the definition I used now.

def is_open_interval (s : set ℝ) := (∃ a b, s = set.Ioo a b) ∨ (∃ a, s = set.Iio a) ∨ (∃ a, s = set.Ioi a)

But I want to find if there is any definition in mathlib

[Yaël Dillies]

What do you want to do with it? Maybe an open set is enough?

[Andrew Yang]

Maybe an open connected set?
Do we have the description of connected subsets of reals in mathlib?

[Yaël Dillies]

docs#set.ord_connected

[ZHAO Jinxiang]

Oh，yes. is_open is what I'm finding