Zulip Chat Archive

Stream: new members

Topic: Category of Topological Spaces


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 13 2019 at 17:30):

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

view this post on Zulip Kenny Lau (Jun 13 2019 at 17:30):

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


Last updated: May 08 2021 at 10:12 UTC