mathlib3

3a0be826 - feat(topology/sheaves): presheaf on indiscrete space is sheaf iff value at empty is terminal (#16694)

feat(topology/sheaves): presheaf on indiscrete space is sheaf iff value at empty is terminal (#16694) + Show that the indiscrete topology (⊤ : topological_space α), defined to be the topology generated by nothing, consists of exactly the empty set and the whole space. + Show that a presheaf on an indiscrete space (in particular the one point space) is a sheaf if its value at the empty set is a terminal object. + Generalize universe level in the converse `is_terminal_of_empty` (which holds for any space). Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>