Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.opens.map_iso_inv_app

Modification history

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_iso_inv_app View on Github →