Zulip Chat Archive

Stream: Is there code for X?

Topic: The closed interval [0,1]


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 09 2021 at 20:55):

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

view this post on Zulip Patrick Massot (Jan 09 2021 at 20:57):

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

view this post on Zulip Reed Mullanix (Jan 09 2021 at 21:00):

Awesome, thanks :)


Last updated: May 07 2021 at 21:10 UTC