put subset in Set module

Author: daniel-levin

Minimathlib/Set.lean

@@ -49,6 +49,11 @@ infixl:65 " ∪ " => Set.union
 postfix:max "ᶜ" => Set.compl
 notation "⋃ " f => Set.iUnion f
 
+-- Basic subset relation
+def subset (s t : Set X) : Prop := ∀ x, x ∈ s → x ∈ t
+
+infixl:50 " ⊆ " => subset
+
 macro "ode_to_grind" : tactic =>
     `(tactic| (
       try unfold Set.compl

Minimathlib/Topology.lean

@@ -31,16 +31,12 @@ open TopologicalSpace
 
 -- De Morgan's laws for closed sets
 theorem isClosed_iUnion : ∀ {ι : Type u} (s : ι → Set X), (∀ i, isClosed (s i)) → isClosed (⋃ s) := by
+  intro ι s i
   sorry
 
 theorem isClosed_union : ∀ s t : Set X, isClosed s → isClosed t → isClosed (s ∪ t) := by
   sorry
 
--- Basic subset relation
-def subset (s t : Set X) : Prop := ∀ x, x ∈ s → x ∈ t
-
-infixl:50 " ⊆ " => subset
-
 -- Neighborhood definitions and properties
 def nhds (x : X) : Set (Set X) := fun s => ∃ t, isOpen t ∧ x ∈ t ∧ t ⊆ s