## Stream: Is there code for X?

### Topic: The closed interval [0,1]

#### Reed Mullanix (Jan 09 2021 at 20:49):

I've been reading some of Hatcher recently, and wanted to mess around with some of it in lean. Do we have the the closed interval [0,1] along with it's topology defined somewhere?

#### Patrick Massot (Jan 09 2021 at 20:55):

Yes, this is (Icc 0 1 : set ℝ).

#### Patrick Massot (Jan 09 2021 at 20:57):

You should have a look at topology.path_connected for instance.

#### Reed Mullanix (Jan 09 2021 at 21:00):

Awesome, thanks :)

Last updated: May 07 2021 at 21:10 UTC