Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 15:41 d952e8bf

View on Github →

chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)

Estimated changes

Modified src/category_theory/category/default.lean

added def category_theory.hom_of_le

added theorem category_theory.le_of_hom

Modified src/category_theory/limits/lattice.lean

Modified src/topology/category/Top/opens.lean

added def topological_space.opens.inf_le_left

added def topological_space.opens.inf_le_right

added def topological_space.opens.le_supr

deleted theorem topological_space.opens.map_comp_hom_app

deleted theorem topological_space.opens.map_comp_inv_app

deleted theorem topological_space.opens.map_id_hom_app

deleted theorem topological_space.opens.map_id_inv_app

modified theorem topological_space.opens.map_obj

added theorem topological_space.opens.to_Top_map