Is there a definition of a general real interval in Mathlib?

Stream: Is there code for X?

[Michael Novak]

I saw that there are closed, open, bounded, unbounded, etc... definitions for intervals in Mathlib, but I couldn't find a definition of a general real interval - a subset I of the real numbers that such that for every two points of I every point in between them is also in I. If there isn't such a definition, then I would love to write one for mathlib and maybe a few theorems like that the other more specific sorts of interval are also intervals by the general definition.

[Aaron Liu]

docs#Set.OrdConnected

[Aaron Liu]

works not just for the real numbers

[Aaron Liu]

if two points are on your set then so is the entire interval between them

[Michael Novak]

Aaron Liu said:

docs#Set.OrdConnected

when I click on this link I get error 404

[Aaron Liu]

sorry I guessed the name wrong twice but it should be correct now (edited original message)

[Michael Novak]

Thank you very much!

[Michael Novak]

btw, sorry for the newbie question: if I want to use this in my lean file, should I write at the beginning of the file:

import Mathlib.Set

even though I already have the line

import Mathlib

or maybe I should even write this

import Mathlib.Set.OrdConnected

?

[Weiyi Wang]

if you already have import Mathlib then you don't need to add any other import of sub files

[Weiyi Wang]

This particular definition is in Mathlib.Order.Interval.Set.Defs if you want to do minimal import, but I don't recommend that for initial exploration because you can miss useful lemmas

[Michael Novak]

If I would like this file eventually to be used in Mathlib, what's the appropriate import line? Is there a convention?

[Kim Morrison]

Once you've finished preparing your file, write #min_imports at the bottom of the file, and replace import Mathlib with what that says.

[Michael Novak]

Kim Morrison said:

Once you've finished preparing your file, write #min_imports at the bottom of the file, and replace import Mathlib with what that says.

Thank you very much!

[Yaël Dillies]

Does #min_imports understand the module system yet?

[Kim Morrison]

No.