Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 11:42 c2a4cf9e

View on Github →

feat(category_theory): lift morphism map proof to concrete categories

Estimated changes

Modified category_theory/examples/topological_spaces.lean

added def category_theory.examples.Top

added def category_theory.examples.open_set.nbhd

added def category_theory.examples.open_set.nbhds

added structure category_theory.examples.open_set

deleted def category_theory.examples.topological_spaces.Top

deleted def category_theory.examples.topological_spaces.nbhd

deleted def category_theory.examples.topological_spaces.nbhds

deleted structure category_theory.examples.topological_spaces.open_set

Modified category_theory/functor.lean

added def category_theory.concrete_functor