Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-16 07:19 361e2163

View on Github →

feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922)

  • rearrange Top
  • oops, import from the future
  • the categories of open sets and of open_nhds
  • missing import
  • restoring opens, adding headers
  • Update src/category_theory/instances/Top/open_nhds.lean Co-Authored-By: semorrison
  • use full_subcategory_inclusion

Estimated changes