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: Dec 20 2023 at 11:08 UTC