Zulip Chat Archive

Stream: Is there code for X?

Topic: Continuous bijective from compact to T1 implies homeomorphis


view this post on Zulip Riccardo Brasca (Mar 10 2021 at 13:01):

I guess that we have somewhere in mathlib the fact that a continuous bijection from a compact space to a separated space is an homeomorphism, but I am not able to find it... does someone know where is it?

view this post on Zulip Sebastien Gouezel (Mar 10 2021 at 13:04):

You have docs#continuous.closed_embedding

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 13:15):

Thank's! It seems a little strange to me that we don't have the literal statement, but may I am missing some subtleties about this part of the library.

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:20):

I think there was a PR recently with a constructor for homeo that did just that. But maybe I misremember.


Last updated: May 07 2021 at 19:12 UTC