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