Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.opens.to_Top_map

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)

Added topological_space.opens.to_Top_map View on Github →