documentation on metric spaces

Stream: maths

[Dean Young]

No, I found all I wanted a few days ago when I wrote up my proof of the CW-approximation theorem. Evidently we didn't have those things. I wanted a proof of the intermediate value theorem to accompany this theorem, so that I could prove that { f : ℝ x ℝ // exp(f.fst) = exp(f.snd) } is weak equivalent to ℤ.

[Dean Young]

So, in sum, enough to prove the intermediate value theorem in a way that appears mostly self contained.