Commit 2022-09-30 08:02 3a0be826

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).