move(topology/sets/*): Move topological types of sets together (#12648)

Move
* `topology.opens` to `topology.sets.opens`
* `topology.compacts` to `topology.sets.closeds` and `topology.sets.compacts`

`closeds` and `clopens` go into `topology.sets.closeds` and `compacts`, `nonempty_compacts`, `positive_compacts` and `compact_opens` go into `topology.sets.compacts`.

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -9,7 +9,7 @@ import ring_theory.nilpotent
 import ring_theory.localization.away
 import ring_theory.ideal.prod
 import ring_theory.ideal.over
-import topology.opens
+import topology.sets.opens
 import topology.sober
 
 /-!

src/category_theory/sites/spaces.lean

@@ -3,11 +3,10 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-
-import topology.opens
 import category_theory.sites.grothendieck
 import category_theory.sites.pretopology
 import category_theory.limits.lattice
+import topology.sets.opens
 
 /-!
 # Grothendieck topology on a topological space

src/measure_theory/measure/content.lean

@@ -5,8 +5,7 @@ Authors: Floris van Doorn
 -/
 import measure_theory.measure.measure_space
 import measure_theory.measure.regular
-import topology.opens
-import topology.compacts
+import topology.sets.compacts
 
 /-!
 # Contents

src/order/category/Frame.lean

@@ -6,7 +6,7 @@ Authors: Yaël Dillies
 import order.category.Lattice
 import order.hom.complete_lattice
 import topology.category.CompHaus
-import topology.opens
+import topology.sets.opens
 
 /-!
 # The category of frames

src/topology/alexandroff.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang, Yury Kudryashov
 -/
 import topology.separation
-import topology.opens
+import topology.sets.opens
 
 /-!
 # The Alexandroff Compactification

src/topology/algebra/group.lean

@@ -6,8 +6,8 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 import group_theory.quotient_group
 import order.filter.pointwise
 import topology.algebra.monoid
-import topology.compacts
 import topology.compact_open
+import topology.sets.compacts
 
 /-!
 # Theory of topological groups

src/topology/algebra/open_subgroup.lean

@@ -3,9 +3,9 @@ Copyright (c) 2019 Johan Commelin All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import topology.opens
 import topology.algebra.ring
 import topology.algebra.filter_basis
+import topology.sets.opens
 /-!
 # Open subgroups of a topological groups
 

src/topology/category/Top/opens.lean

@@ -3,10 +3,10 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import topology.opens
 import category_theory.category.preorder
 import category_theory.eq_to_hom
 import topology.category.Top.epi_mono
+import topology.sets.opens
 
 /-!
 # The category of open sets in a topological space.

src/topology/local_homeomorph.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import data.equiv.local_equiv
-import topology.opens
+import topology.sets.opens
 
 /-!
 # Local homeomorphisms

src/topology/metric_space/closeds.lean

@@ -3,9 +3,9 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import topology.metric_space.hausdorff_distance
-import topology.compacts
 import analysis.specific_limits
+import topology.metric_space.hausdorff_distance
+import topology.sets.compacts
 
 /-!
 # Closed subsets

src/topology/metric_space/kuratowski.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.lp_space
-import topology.compacts
+import topology.sets.compacts
 
 /-!
 # The Kuratowski embedding

src/topology/sets/closeds.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Yaël Dillies
+-/
+import topology.sets.opens
+
+/-!
+# Closed sets
+
+We define a few types of closed sets in a topological space.
+
+## Main Definitions
+
+For a topological space `α`,
+* `closeds α`: The type of closed sets.
+* `clopens α`: The type of clopen sets.
+-/
+
+open set
+
+variables {α β : Type*} [topological_space α] [topological_space β]
+
+namespace topological_space
+
+/-! ### Closed sets -/
+
+/-- The type of closed subsets of a topological space. -/
+structure closeds (α : Type*) [topological_space α] :=
+(carrier : set α)
+(closed' : is_closed carrier)
+
+namespace closeds
+variables {α}
+
+instance : set_like (closeds α) α :=
+{ coe := closeds.carrier,
+  coe_injective' := λ s t h, by { cases s, cases t, congr' } }
+
+lemma closed (s : closeds α) : is_closed (s : set α) := s.closed'
+
+@[ext] protected lemma ext {s t : closeds α} (h : (s : set α) = t) : s = t := set_like.ext' h
+
+@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl
+
+instance : has_sup (closeds α) := ⟨λ s t, ⟨s ∪ t, s.closed.union t.closed⟩⟩
+instance : has_inf (closeds α) := ⟨λ s t, ⟨s ∩ t, s.closed.inter t.closed⟩⟩
+instance : has_top (closeds α) := ⟨⟨univ, is_closed_univ⟩⟩
+instance : has_bot (closeds α) := ⟨⟨∅, is_closed_empty⟩⟩
+
+instance : distrib_lattice (closeds α) :=
+set_like.coe_injective.distrib_lattice _ (λ _ _, rfl) (λ _ _, rfl)
+instance : bounded_order (closeds α) := bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl
+
+/-- The type of closed sets is inhabited, with default element the empty set. -/
+instance : inhabited (closeds α) := ⟨⊥⟩
+
+@[simp] lemma coe_sup (s t : closeds α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
+@[simp] lemma coe_inf (s t : closeds α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
+@[simp] lemma coe_top : (↑(⊤ : closeds α) : set α) = univ := rfl
+@[simp] lemma coe_bot : (↑(⊥ : closeds α) : set α) = ∅ := rfl
+
+end closeds
+
+/-! ### Clopen sets -/
+
+/-- The type of clopen sets of a topological space. -/
+structure clopens (α : Type*) [topological_space α] :=
+(carrier : set α)
+(clopen' : is_clopen carrier)
+
+namespace clopens
+
+instance : set_like (clopens α) α :=
+{ coe := λ s, s.carrier,
+  coe_injective' := λ s t h, by { cases s, cases t, congr' } }
+
+lemma clopen (s : clopens α) : is_clopen (s : set α) := s.clopen'
+
+/-- Reinterpret a compact open as an open. -/
+@[simps] def to_opens (s : clopens α) : opens α := ⟨s, s.clopen.is_open⟩
+
+@[ext] protected lemma ext {s t : clopens α} (h : (s : set α) = t) : s = t := set_like.ext' h
+
+@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl
+
+instance : has_sup (clopens α) := ⟨λ s t, ⟨s ∪ t, s.clopen.union t.clopen⟩⟩
+instance : has_inf (clopens α) := ⟨λ s t, ⟨s ∩ t, s.clopen.inter t.clopen⟩⟩
+instance : has_top (clopens α) := ⟨⟨⊤, is_clopen_univ⟩⟩
+instance : has_bot (clopens α) := ⟨⟨⊥, is_clopen_empty⟩⟩
+instance : has_sdiff (clopens α) := ⟨λ s t, ⟨s \ t, s.clopen.diff t.clopen⟩⟩
+instance : has_compl (clopens α) := ⟨λ s, ⟨sᶜ, s.clopen.compl⟩⟩
+
+instance : boolean_algebra (clopens α) :=
+set_like.coe_injective.boolean_algebra _ (λ _ _, rfl) (λ _ _, rfl) rfl rfl (λ _, rfl) (λ _ _, rfl)
+
+@[simp] lemma coe_sup (s t : clopens α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
+@[simp] lemma coe_inf (s t : clopens α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
+@[simp] lemma coe_top : (↑(⊤ : clopens α) : set α) = univ := rfl
+@[simp] lemma coe_bot : (↑(⊥ : clopens α) : set α) = ∅ := rfl
+@[simp] lemma coe_sdiff (s t : clopens α) : (↑(s \ t) : set α) = s \ t := rfl
+@[simp] lemma coe_compl (s : clopens α) : (↑sᶜ : set α) = sᶜ := rfl
+
+instance : inhabited (clopens α) := ⟨⊥⟩
+
+end clopens
+end topological_space

src/topology/compacts.lean → src/topology/sets/compacts.lean

@@ -3,23 +3,21 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yaël Dillies
 -/
-import topology.opens
+import topology.sets.closeds
 
 /-!
 # Compact sets
 
-We define a few types of sets in a topological space.
+We define a few types of compact sets in a topological space.
 
 ## Main Definitions
 
 For a topological space `α`,
-- `closeds α`: The type of closed sets.
-- `compacts α`: The type of compact sets.
-- `nonempty_compacts α`: The type of non-empty compact sets.
-- `positive_compacts α`: The type of compact sets with non-empty interior.
-- `clopens α`: The type of clopen sets.
-- `compact_opens α`: The type of compact open sets. This is a central object of study in the
-  context of spectral spaces.
+* `compacts α`: The type of compact sets.
+* `nonempty_compacts α`: The type of non-empty compact sets.
+* `positive_compacts α`: The type of compact sets with non-empty interior.
+* `compact_opens α`: The type of compact open sets. This is a central object in the study of
+  spectral spaces.
 -/
 
 open set
@@ -28,45 +26,6 @@ variables {α β : Type*} [topological_space α] [topological_space β]
 
 namespace topological_space
 
-/-! ### Closed sets -/
-
-/-- The type of closed subsets of a topological space. -/
-structure closeds (α : Type*) [topological_space α] :=
-(carrier : set α)
-(closed' : is_closed carrier)
-
-namespace closeds
-variables {α}
-
-instance : set_like (closeds α) α :=
-{ coe := closeds.carrier,
-  coe_injective' := λ s t h, by { cases s, cases t, congr' } }
-
-lemma closed (s : closeds α) : is_closed (s : set α) := s.closed'
-
-@[ext] protected lemma ext {s t : closeds α} (h : (s : set α) = t) : s = t := set_like.ext' h
-
-@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl
-
-instance : has_sup (closeds α) := ⟨λ s t, ⟨s ∪ t, s.closed.union t.closed⟩⟩
-instance : has_inf (closeds α) := ⟨λ s t, ⟨s ∩ t, s.closed.inter t.closed⟩⟩
-instance : has_top (closeds α) := ⟨⟨univ, is_closed_univ⟩⟩
-instance : has_bot (closeds α) := ⟨⟨∅, is_closed_empty⟩⟩
-
-instance : distrib_lattice (closeds α) :=
-set_like.coe_injective.distrib_lattice _ (λ _ _, rfl) (λ _ _, rfl)
-instance : bounded_order (closeds α) := bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl
-
-/-- The type of closed sets is inhabited, with default element the empty set. -/
-instance : inhabited (closeds α) := ⟨⊥⟩
-
-@[simp] lemma coe_sup (s t : closeds α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
-@[simp] lemma coe_inf (s t : closeds α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
-@[simp] lemma coe_top : (↑(⊤ : closeds α) : set α) = univ := rfl
-@[simp] lemma coe_bot : (↑(⊥ : closeds α) : set α) = ∅ := rfl
-
-end closeds
-
 /-! ### Compact sets -/
 
 /-- The type of compact sets of a topological space. -/
@@ -240,49 +199,6 @@ let ⟨s, hs⟩ := exists_compact_subset is_open_univ $ mem_univ (classical.arbi
 
 end positive_compacts
 
-/-! ### Clopen sets -/
-
-/-- The type of clopen sets of a topological space. -/
-structure clopens (α : Type*) [topological_space α] :=
-(carrier : set α)
-(clopen' : is_clopen carrier)
-
-namespace clopens
-
-instance : set_like (clopens α) α :=
-{ coe := λ s, s.carrier,
-  coe_injective' := λ s t h, by { cases s, cases t, congr' } }
-
-lemma clopen (s : clopens α) : is_clopen (s : set α) := s.clopen'
-
-/-- Reinterpret a compact open as an open. -/
-@[simps] def to_opens (s : clopens α) : opens α := ⟨s, s.clopen.is_open⟩
-
-@[ext] protected lemma ext {s t : clopens α} (h : (s : set α) = t) : s = t := set_like.ext' h
-
-@[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl
-
-instance : has_sup (clopens α) := ⟨λ s t, ⟨s ∪ t, s.clopen.union t.clopen⟩⟩
-instance : has_inf (clopens α) := ⟨λ s t, ⟨s ∩ t, s.clopen.inter t.clopen⟩⟩
-instance : has_top (clopens α) := ⟨⟨⊤, is_clopen_univ⟩⟩
-instance : has_bot (clopens α) := ⟨⟨⊥, is_clopen_empty⟩⟩
-instance : has_sdiff (clopens α) := ⟨λ s t, ⟨s \ t, s.clopen.diff t.clopen⟩⟩
-instance : has_compl (clopens α) := ⟨λ s, ⟨sᶜ, s.clopen.compl⟩⟩
-
-instance : boolean_algebra (clopens α) :=
-set_like.coe_injective.boolean_algebra _ (λ _ _, rfl) (λ _ _, rfl) rfl rfl (λ _, rfl) (λ _ _, rfl)
-
-@[simp] lemma coe_sup (s t : clopens α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
-@[simp] lemma coe_inf (s t : clopens α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
-@[simp] lemma coe_top : (↑(⊤ : clopens α) : set α) = univ := rfl
-@[simp] lemma coe_bot : (↑(⊥ : clopens α) : set α) = ∅ := rfl
-@[simp] lemma coe_sdiff (s t : clopens α) : (↑(s \ t) : set α) = s \ t := rfl
-@[simp] lemma coe_compl (s : clopens α) : (↑sᶜ : set α) = sᶜ := rfl
-
-instance : inhabited (clopens α) := ⟨⊥⟩
-
-end clopens
-
 /-! ### Compact open sets -/
 
 /-- The type of compact open sets of a topological space. This is useful in non Hausdorff contexts,