Zulip Chat Archive
Stream: mathlib4
Topic: documentation on the unit interval and metric spaces
Notification Bot (Feb 10 2023 at 23:08):
This topic was moved to #maths > documentation on the unit interval and metric spaces by Yury G. Kudryashov.
Last updated: Dec 20 2023 at 11:08 UTC