Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.opens.map_comp_inv_app

Modification history

2020-08-05 15:41
src/topology/category/Top/opens.lean
chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)
Deleted topological_space.opens.map_comp_inv_appView on Github →
2020-05-31 06:22
src/topology/category/Top/opens.lean
chore(*): split long lines (#2883) …
Modified topological_space.opens.map_comp_inv_appView 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) …
Added topological_space.opens.map_comp_inv_appView on Github →