Zulip Chat Archive

Stream: new members

Topic: opens as a category


view this post on Zulip Kenny Lau (Aug 31 2020 at 18:41):

Given an U : opens X, what is the canonical way to produce U \hom \top?

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:42):

hom_of_le?

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:42):

But maybe it has a dedicated name.

view this post on Zulip Scott Morrison (Aug 31 2020 at 22:46):

There should be more wrappers below src#topological_space.opens.le_supr, I guess.

view this post on Zulip Scott Morrison (Aug 31 2020 at 22:47):

in particular le_top.


Last updated: May 10 2021 at 18:22 UTC