Stream: Is there code for X?
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?
Sebastien Gouezel (Mar 10 2021 at 13:04):
You have docs#continuous.closed_embedding
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.
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