feat: port Topology.Sheaves.Presheaf (#3828)

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

Author: 4 people

Mathlib.lean

@@ -2218,6 +2218,8 @@ import Mathlib.Topology.Sets.Compacts
 import Mathlib.Topology.Sets.Opens
 import Mathlib.Topology.Sets.Order
 import Mathlib.Topology.Sheaves.Abelian
+import Mathlib.Topology.Sheaves.Init
+import Mathlib.Topology.Sheaves.Presheaf
 import Mathlib.Topology.ShrinkingLemma
 import Mathlib.Topology.Sober
 import Mathlib.Topology.Spectral.Hom

Mathlib/Topology/Sheaves/Init.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2023 Jujian Zhang All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+
+import Aesop
+
+/-!
+# Rule sets related to topological (pre)sheaves
+
+This module defines the `Restrict` Aesop rule set. Aesop rule sets only become
+visible once the file in which they're declared is imported, so we must put this
+declaration into its own file.
+-/
+
+/- to prove subset relations -/
+declare_aesop_rule_sets [Restrict]