documentation on the unit interval and metric spaces

Stream: maths

[Dean Young]

I'm looking for documentation on the unit interval and metric spaces. I want to make some things with manifolds with boundaries.

[Jireh Loreaux]

Do you know about the docs#metric_space ? What documentation are you looking for specifically?

[Jireh Loreaux]

For manifolds I think it starts with docs#charted_space, but the geometry people will know more, e.g., @Oliver Nash

[Notification Bot]

This topic was moved here from #mathlib4 > documentation on the unit interval and metric spaces by Yury G. Kudryashov.

[Oliver Nash]

@Kind Bubble Is there anything specific I can help with Dean?