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: May 02 2025 at 03:31 UTC