Zulip Chat Archive
Stream: new members
Topic: opens as a category
Kenny Lau (Aug 31 2020 at 18:41):
Given an U : opens X, what is the canonical way to produce U \hom \top?
Johan Commelin (Aug 31 2020 at 18:42):
hom_of_le?
Johan Commelin (Aug 31 2020 at 18:42):
But maybe it has a dedicated name.
Scott Morrison (Aug 31 2020 at 22:46):
There should be more wrappers below src#topological_space.opens.le_supr, I guess.
Scott Morrison (Aug 31 2020 at 22:47):
in particular le_top.
Last updated: Dec 20 2023 at 11:08 UTC