Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.instances.Top.discrete

Modification history

2019-05-31 06:43
src/topology/Top/basic.lean
chore(category_theory): move all instances (e.g. Top, CommRing, Meas) into the root namespace (#1074) …
Deleted category_theory.instances.Top.discreteView on Github →
2019-04-16 07:19
src/category_theory/instances/Top/basic.lean
feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922) …
Modified category_theory.instances.Top.discreteView on Github →
2019-01-30 18:20
src/category_theory/instances/topological_spaces.lean
refactor(category_theory/instances): rename `examples` to `instances`
Added category_theory.instances.Top.discreteView on Github →