Zulip Chat Archive
Stream: mathlib4
Topic: docs4#TopologicalSpace.Opens.leSupr
Jujian Zhang (May 27 2023 at 15:00):
Is docs4#TopologicalSpace.Opens.leSupr named incorrectly?
Yaël Dillies (May 27 2023 at 15:04):
Yes. Should be .le_iSup.
Last updated: May 02 2025 at 03:31 UTC