Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 11:42 d91428c2

View on Github →

feat(category_theory): the category of topological spaces, and of neighbourhoods of a point. also the category of commutative rings

Estimated changes

Modified analysis/topology/topological_structures.lean

Created category_theory/examples/rings.lean

added def category_theory.examples.CommRing

added def category_theory.examples.comm_ring_hom.comp

added theorem category_theory.examples.comm_ring_hom.comp_map

added theorem category_theory.examples.comm_ring_hom.ext

added def category_theory.examples.comm_ring_hom.id

added theorem category_theory.examples.comm_ring_hom.id_map

added theorem category_theory.examples.comm_ring_hom.map_add

added theorem category_theory.examples.comm_ring_hom.map_mul

added theorem category_theory.examples.comm_ring_hom.map_one

added structure category_theory.examples.comm_ring_hom

Created category_theory/examples/topological_spaces.lean

added def category_theory.examples.topological_spaces.Top

added theorem category_theory.examples.topological_spaces.continuous_map.ext

added structure category_theory.examples.topological_spaces.continuous_map

added def category_theory.examples.topological_spaces.nbhd

added def category_theory.examples.topological_spaces.nbhds

added structure category_theory.examples.topological_spaces.open_set