Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Def
topological_space.opens.map_id
Modification history
2019-09-01 11:29
src/topology/Top/opens.lean
chore(category_theory/notation): consistently use notation for functor.id (#1378) …
Modified
topological_space.opens.map_id
View on Github →
2019-04-16 07:19
src/category_theory/instances/Top/opens.lean
feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922) …
Modified
topological_space.opens.map_id
View on Github →
2018-12-20 23:12
category_theory/examples/topological_spaces.lean
feat(category_theory): assorted small changes from the old limits PR (#512)
Added
topological_space.opens.map_id
View on Github →