Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC