chore(AlexandrovDiscrete): move exterior to new files (#16957)

I'm going to use `exterior` in files that don't need to know about `AlexandrovDiscrete`.

Author: urkud

Mathlib.lean

@@ -4542,6 +4542,7 @@ import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
+import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.Lindelof
 import Mathlib.Topology.Compactness.LocallyCompact
 import Mathlib.Topology.Compactness.Paracompact
@@ -4592,6 +4593,7 @@ import Mathlib.Topology.EMetricSpace.Lipschitz
 import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Topology.EMetricSpace.Pi
 import Mathlib.Topology.ExtendFrom
+import Mathlib.Topology.Exterior
 import Mathlib.Topology.ExtremallyDisconnected
 import Mathlib.Topology.FiberBundle.Basic
 import Mathlib.Topology.FiberBundle.Constructions

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -5,9 +5,8 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Set.Image
 import Mathlib.Topology.Bases
-import Mathlib.Tactic.Peel
 import Mathlib.Topology.Inseparable
-import Mathlib.Topology.Compactness.Compact
+import Mathlib.Topology.Compactness.Exterior
 
 /-!
 # Alexandrov-discrete topological spaces
@@ -21,8 +20,6 @@ minimal neighborhood, which we call the *exterior* of the set.
 ## Main declarations
 
 * `AlexandrovDiscrete`: Prop-valued typeclass for a topological space to be Alexandrov-discrete
-* `exterior`: Intersection of all neighborhoods of a set. When the space is Alexandrov-discrete,
-  this is the minimal neighborhood of the set.
 
 ## Notes
 
@@ -119,89 +116,6 @@ end AlexandrovDiscrete
 
 variable {s t : Set α} {a x y : α}
 
-/-- The *exterior* of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete
-space, this is the smallest neighborhood of the set.
-
-Note that this construction is unnamed in the literature. We choose the name in analogy to
-`interior`. -/
-def exterior (s : Set α) : Set α := (𝓝ˢ s).ker
-
-lemma exterior_singleton_eq_ker_nhds (a : α) : exterior {a} = (𝓝 a).ker := by simp [exterior]
-
-@[simp]
-theorem mem_exterior_singleton : x ∈ exterior {y} ↔ x ⤳ y := by
-  rw [exterior_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]
-
-lemma exterior_def (s : Set α) : exterior s = ⋂₀ {t : Set α | IsOpen t ∧ s ⊆ t} :=
-  (hasBasis_nhdsSet _).ker.trans sInter_eq_biInter.symm
-
-lemma mem_exterior : a ∈ exterior s ↔ ∀ U, IsOpen U → s ⊆ U → a ∈ U := by simp [exterior_def]
-
-lemma subset_exterior_iff : s ⊆ exterior t ↔ ∀ U, IsOpen U → t ⊆ U → s ⊆ U := by
-  simp [exterior_def]
-
-lemma subset_exterior : s ⊆ exterior s := subset_exterior_iff.2 fun _ _ ↦ id
-
-lemma exterior_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t := by
-  rw [exterior_def]; exact sInter_subset_of_mem ⟨h₂, h₁⟩
-
-lemma IsOpen.exterior_eq (h : IsOpen s) : exterior s = s :=
-  (exterior_minimal Subset.rfl h).antisymm subset_exterior
-
-lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
-  ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩
-
-@[deprecated (since := "2024-09-18")] alias IsOpen.exterior_subset_iff := IsOpen.exterior_subset
-
-@[simp]
-theorem exterior_iUnion {ι : Sort*} (s : ι → Set α) :
-    exterior (⋃ i, s i) = ⋃ i, exterior (s i) := by
-  simp only [exterior, nhdsSet_iUnion, ker_iSup]
-
-@[simp]
-theorem exterior_union (s t : Set α) : exterior (s ∪ t) = exterior s ∪ exterior t := by
-  simp only [exterior, nhdsSet_union, ker_sup]
-
-@[simp]
-theorem exterior_sUnion (S : Set (Set α)) : exterior (⋃₀ S) = ⋃ s ∈ S, exterior s := by
-  simp only [sUnion_eq_biUnion, exterior_iUnion]
-
-theorem mem_exterior_iff_specializes : a ∈ exterior s ↔ ∃ b ∈ s, a ⤳ b := calc
-  a ∈ exterior s ↔ a ∈ exterior (⋃ x ∈ s, {x}) := by simp
-  _ ↔ ∃ b ∈ s, a ⤳ b := by
-    simp only [exterior_iUnion, mem_exterior_singleton, mem_iUnion₂, exists_prop]
-
-@[mono] lemma exterior_mono : Monotone (exterior : Set α → Set α) :=
-  fun _s _t h ↦ ker_mono <| nhdsSet_mono h
-
-/-- This name was used to be used for the `Iff` version,
-see `exterior_subset_exterior_iff_nhdsSet`.
--/
-@[gcongr] lemma exterior_subset_exterior (h : s ⊆ t) : exterior s ⊆ exterior t := exterior_mono h
-
-@[simp] lemma exterior_subset_exterior_iff_nhdsSet : exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t := by
-  simp (config := {contextual := true}) only [subset_exterior_iff, (hasBasis_nhdsSet _).ge_iff,
-    and_imp, IsOpen.mem_nhdsSet, IsOpen.exterior_subset]
-
-theorem exterior_eq_exterior_iff_nhdsSet : exterior s = exterior t ↔ 𝓝ˢ s = 𝓝ˢ t := by
-  simp [le_antisymm_iff]
-
-lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y} := by
-  simp [Specializes]
-
-@[simp] lemma exterior_empty : exterior (∅ : Set α) = ∅ := isOpen_empty.exterior_eq
-@[simp] lemma exterior_univ : exterior (univ : Set α) = univ := isOpen_univ.exterior_eq
-
-@[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ :=
-  ⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩
-
-@[simp] lemma nhdsSet_exterior (s : Set α) : 𝓝ˢ (exterior s) = 𝓝ˢ s := by
-  refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_exterior)
-  exact fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.exterior_subset.2 hsU
-
-@[simp] lemma exterior_exterior (s : Set α) : exterior (exterior s) = exterior s := by
-  simp only [exterior_eq_exterior_iff_nhdsSet, nhdsSet_exterior]
-
 lemma Inducing.alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : Inducing f) :
     AlexandrovDiscrete β where
   isOpen_sInter S hS := by
@@ -210,18 +124,6 @@ lemma Inducing.alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : I
     refine ⟨_, isOpen_iInter₂ hU, ?_⟩
     simp_rw [preimage_iInter, htU, sInter_eq_biInter]
 
-theorem IsCompact.exterior_iff : IsCompact (exterior s) ↔ IsCompact s := by
-  simp only [isCompact_iff_finite_subcover]
-  peel with ι U hUo
-  simp only [(isOpen_iUnion hUo).exterior_subset,
-    (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).exterior_subset]
-
-protected alias ⟨IsCompact.of_exterior, IsCompact.exterior⟩ := IsCompact.exterior_iff
-
-@[deprecated IsCompact.exterior (since := "2024-09-18")]
-lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) :=
-  hs.isCompact.exterior
-
 end
 
 lemma AlexandrovDiscrete.sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁)
@@ -283,7 +185,7 @@ instance AlexandrovDiscrete.toFirstCountable : FirstCountableTopology α where
 instance AlexandrovDiscrete.toLocallyCompactSpace : LocallyCompactSpace α where
   local_compact_nhds a _U hU := ⟨exterior {a},
     isOpen_exterior.mem_nhds <| subset_exterior <| mem_singleton _,
-      exterior_singleton_subset_iff_mem_nhds.2 hU, (finite_singleton _).isCompact.exterior⟩
+      exterior_singleton_subset_iff_mem_nhds.2 hU, isCompact_singleton.exterior⟩
 
 instance Subtype.instAlexandrovDiscrete {p : α → Prop} : AlexandrovDiscrete {a // p a} :=
   inducing_subtype_val.alexandrovDiscrete

Mathlib/Topology/Compactness/Exterior.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Tactic.Peel
+import Mathlib.Topology.Compactness.Compact
+import Mathlib.Topology.Exterior
+
+/-!
+# Compactness of the exterior of a set
+
+In this file we prove that the exterior of a set
+(defined as the intersection of all of its neighborhoods)
+is a compact set if and only if the original set is a compact set.
+-/
+
+variable {X : Type*} [TopologicalSpace X] {s : Set X}
+
+theorem IsCompact.exterior_iff : IsCompact (exterior s) ↔ IsCompact s := by
+  simp only [isCompact_iff_finite_subcover]
+  peel with ι U hUo
+  simp only [(isOpen_iUnion hUo).exterior_subset,
+    (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).exterior_subset]
+
+protected alias ⟨IsCompact.of_exterior, IsCompact.exterior⟩ := IsCompact.exterior_iff
+
+@[deprecated IsCompact.exterior (since := "2024-09-18")]
+lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) :=
+  hs.isCompact.exterior

Mathlib/Topology/Defs/Filter.lean

@@ -29,6 +29,12 @@ as well as other definitions that rely on `Filter`s.
   denoted by `𝓝ˢ s` in the `Topology` scope.
   A set `t` is called a neighborhood of `s`, if it includes an open set that includes `s`.
 
+* `exterior s`: The *exterior* of a set is the intersection of all its neighborhoods.
+  In an Alexandrov-discrete space, this is the smallest neighborhood of the set.
+
+  Note that this construction is unnamed in the literature.
+  We choose the name in analogy to `interior`.
+
 ### Continuity at a point
 
 * `ContinuousAt f x`: a function `f` is continuous at a point `x`,
@@ -146,6 +152,13 @@ def nhdsSet (s : Set X) : Filter X :=
 
 @[inherit_doc] scoped[Topology] notation "𝓝ˢ" => nhdsSet
 
+/-- The *exterior* of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete
+space, this is the smallest neighborhood of the set.
+
+Note that this construction is unnamed in the literature. We choose the name in analogy to
+`interior`. -/
+def exterior (s : Set X) : Set X := (𝓝ˢ s).ker
+
 /-- A function between topological spaces is continuous at a point `x₀`
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
 @[fun_prop]

Mathlib/Topology/Exterior.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Yury Kudryashov
+-/
+import Mathlib.Topology.NhdsSet
+import Mathlib.Topology.Inseparable
+
+/-!
+# Exterior of a set
+
+We define `exterior s` to be the intersection of all neighborhoods of `s`,
+see `Topology/Defs/Filter`.
+Note that this construction has no standard name in the literature.
+
+In this file we prove basic properties of this operation.
+-/
+
+open Set Filter
+open scoped Topology
+
+variable {X : Type*} [TopologicalSpace X] {s t : Set X} {x y : X}
+
+lemma exterior_singleton_eq_ker_nhds (x : X) : exterior {x} = (𝓝 x).ker := by simp [exterior]
+
+@[simp]
+theorem mem_exterior_singleton : x ∈ exterior {y} ↔ x ⤳ y := by
+  rw [exterior_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]
+
+lemma exterior_def (s : Set X) : exterior s = ⋂₀ {t : Set X | IsOpen t ∧ s ⊆ t} :=
+  (hasBasis_nhdsSet _).ker.trans sInter_eq_biInter.symm
+
+lemma mem_exterior : x ∈ exterior s ↔ ∀ U, IsOpen U → s ⊆ U → x ∈ U := by simp [exterior_def]
+
+lemma subset_exterior_iff : s ⊆ exterior t ↔ ∀ U, IsOpen U → t ⊆ U → s ⊆ U := by
+  simp [exterior_def]
+
+lemma subset_exterior : s ⊆ exterior s := subset_exterior_iff.2 fun _ _ ↦ id
+
+lemma exterior_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t := by
+  rw [exterior_def]; exact sInter_subset_of_mem ⟨h₂, h₁⟩
+
+lemma IsOpen.exterior_eq (h : IsOpen s) : exterior s = s :=
+  (exterior_minimal Subset.rfl h).antisymm subset_exterior
+
+lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
+  ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩
+
+@[deprecated (since := "2024-09-18")] alias IsOpen.exterior_subset_iff := IsOpen.exterior_subset
+
+@[simp]
+theorem exterior_iUnion {ι : Sort*} (s : ι → Set X) :
+    exterior (⋃ i, s i) = ⋃ i, exterior (s i) := by
+  simp only [exterior, nhdsSet_iUnion, ker_iSup]
+
+@[simp]
+theorem exterior_union (s t : Set X) : exterior (s ∪ t) = exterior s ∪ exterior t := by
+  simp only [exterior, nhdsSet_union, ker_sup]
+
+@[simp]
+theorem exterior_sUnion (S : Set (Set X)) : exterior (⋃₀ S) = ⋃ s ∈ S, exterior s := by
+  simp only [sUnion_eq_biUnion, exterior_iUnion]
+
+theorem mem_exterior_iff_specializes : x ∈ exterior s ↔ ∃ y ∈ s, x ⤳ y := calc
+  x ∈ exterior s ↔ x ∈ exterior (⋃ y ∈ s, {y}) := by simp
+  _ ↔ ∃ y ∈ s, x ⤳ y := by
+    simp only [exterior_iUnion, mem_exterior_singleton, mem_iUnion₂, exists_prop]
+
+@[mono] lemma exterior_mono : Monotone (exterior : Set X → Set X) :=
+  fun _s _t h ↦ ker_mono <| nhdsSet_mono h
+
+/-- This name was used to be used for the `Iff` version,
+see `exterior_subset_exterior_iff_nhdsSet`.
+-/
+@[gcongr] lemma exterior_subset_exterior (h : s ⊆ t) : exterior s ⊆ exterior t := exterior_mono h
+
+@[simp] lemma exterior_subset_exterior_iff_nhdsSet : exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t := by
+  simp (config := {contextual := true}) only [subset_exterior_iff, (hasBasis_nhdsSet _).ge_iff,
+    and_imp, IsOpen.mem_nhdsSet, IsOpen.exterior_subset]
+
+theorem exterior_eq_exterior_iff_nhdsSet : exterior s = exterior t ↔ 𝓝ˢ s = 𝓝ˢ t := by
+  simp [le_antisymm_iff]
+
+lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y} := by
+  simp [Specializes]
+
+@[simp] lemma exterior_empty : exterior (∅ : Set X) = ∅ := isOpen_empty.exterior_eq
+@[simp] lemma exterior_univ : exterior (univ : Set X) = univ := isOpen_univ.exterior_eq
+
+@[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ :=
+  ⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩
+
+@[simp] lemma nhdsSet_exterior (s : Set X) : 𝓝ˢ (exterior s) = 𝓝ˢ s := by
+  refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_exterior)
+  exact fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.exterior_subset.2 hsU
+
+@[simp] lemma exterior_exterior (s : Set X) : exterior (exterior s) = exterior s := by
+  simp only [exterior_eq_exterior_iff_nhdsSet, nhdsSet_exterior]