continuous map to \top

Stream: Is there code for X?

[Kenny Lau]

Do we know that the map from a topological space to its top subspace (the whole subspace) is continuous?

[Reid Barton]

I don't know if we have this exact statement, but the easy way to prove it is to note it's the factorization of a continuous map (the identity) through an embedding

[Reid Barton]

docs#embedding.continuous_iff