Zulip Chat Archive

Stream: new members

Topic: Category of Topological Spaces

Ken Lee (Jun 13 2019 at 17:28):

Where can I find the definition of the category of topological spaces in mathlib? It doesn't seem to be in category_theory.

Kenny Lau (Jun 13 2019 at 17:30):

/-- The category of topological spaces and continuous maps. -/
@[reducible] def Top : Type (u+1) := bundled topological_space

Kenny Lau (Jun 13 2019 at 17:30):

https://github.com/leanprover-community/mathlib/blob/master/src/topology/Top/basic.lean#L14

Kenny Lau (Jun 13 2019 at 17:30):

per https://github.com/leanprover-community/mathlib/commit/2db435d8ea939af43fb215dea93543fe36ce516e

Last updated: Dec 20 2023 at 11:08 UTC