[Merged by Bors] - feat(Topology/LocallyClosed): Define locally closed sets

Mathlib.lean

@@ -4343,6 +4343,7 @@ import Mathlib.Topology.IsLocalHomeomorph
 import Mathlib.Topology.KrullDimension
 import Mathlib.Topology.List
 import Mathlib.Topology.LocalAtTarget
+import Mathlib.Topology.LocallyClosed
 import Mathlib.Topology.LocallyConstant.Algebra
 import Mathlib.Topology.LocallyConstant.Basic
 import Mathlib.Topology.LocallyFinite

Mathlib/Topology/Basic.lean

@@ -701,8 +701,10 @@ theorem frontier_subset_closure : frontier s ⊆ closure s :=
   diff_subset
 #align frontier_subset_closure frontier_subset_closure
 
-theorem IsClosed.frontier_subset (hs : IsClosed s) : frontier s ⊆ s :=
-  frontier_subset_closure.trans hs.closure_eq.subset
+theorem frontier_subset_iff_isClosed : frontier s ⊆ s ↔ IsClosed s := by
+  rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]
+
+alias ⟨_, IsClosed.frontier_subset⟩ := frontier_subset_iff_isClosed
 #align is_closed.frontier_subset IsClosed.frontier_subset
 
 theorem frontier_closure_subset : frontier (closure s) ⊆ frontier s :=
@@ -752,6 +754,10 @@ theorem IsOpen.inter_frontier_eq (hs : IsOpen s) : s ∩ frontier s = ∅ := by
   rw [hs.frontier_eq, inter_diff_self]
 #align is_open.inter_frontier_eq IsOpen.inter_frontier_eq
 
+theorem disjoint_frontier_iff_isOpen : Disjoint (frontier s) s ↔ IsOpen s := by
+  rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
+    frontier_compl, subset_compl_iff_disjoint_right]
+
 /-- The frontier of a set is closed. -/
 theorem isClosed_frontier : IsClosed (frontier s) := by
   rw [frontier_eq_closure_inter_closure]; exact IsClosed.inter isClosed_closure isClosed_closure

Mathlib/Topology/Constructions.lean

@@ -1249,6 +1249,13 @@ theorem QuotientMap.restrictPreimage_isOpen {f : X → Y} (hf : QuotientMap f)
     (hs.preimage hf.continuous).openEmbedding_subtype_val.open_iff_image_open,
     image_val_preimage_restrictPreimage]
 
+open scoped Set.Notation in
+lemma isClosed_preimage_val {s t : Set X} : IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t := by
+  rw [← closure_eq_iff_isClosed, embedding_subtype_val.closure_eq_preimage_closure_image,
+    ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe,
+    Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff,
+    and_iff_right]
+  exacts [Set.inter_subset_left, Set.subset_inter Set.inter_subset_left subset_closure]
 end Subtype
 
 section Quotient

Mathlib/Topology/LocallyClosed.lean

@@ -0,0 +1,214 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.Topology.LocalAtTarget
+
+/-!
+# Locally closed sets
+
+## Main definitions
+
+* `IsLocallyClosed`: Predicate saying that a set is locally closed
+
+## Main results
+
+* `isLocallyClosed_tfae`:
+  A set `s` is locally closed if one of the equivalent conditions below hold
+  1. It is the intersection of some open set and some closed set.
+  2. The coborder `(closure s \ s)ᶜ` is open.
+  3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
+  4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
+  5. `s` is open in the closure of `s`.
+
+-/
+
+variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β}
+
+open scoped Topology Set.Notation
+
+open Set
+
+/--
+The coborder is defined as the complement of `closure s \ s`,
+or the union of `s` and the complement of `∂(s)`.
+This is the largest set such that `s` is closed in, and `s` is locally closed if and only if
+`coborder s` is open.
+
+This is unnamed in the literature, and this name is due to the fact that `coborder s = (border sᶜ)ᶜ`
+where `border s = s \ interior s` is the border in the sense of Hausdorff.
+-/
+def coborder (s : Set α) : Set α :=
+  (closure s \ s)ᶜ
+
+lemma subset_coborder :
+    s ⊆ coborder s := by
+  rw [coborder, subset_compl_iff_disjoint_right]
+  exact disjoint_sdiff_self_right
+
+lemma coborder_inter_closure :
+    coborder s ∩ closure s = s := by
+  rw [coborder, ← diff_eq_compl_inter, diff_diff_right_self, inter_eq_right]
+  exact subset_closure
+
+lemma closure_inter_coborder :
+    closure s ∩ coborder s = s := by
+  rw [inter_comm, coborder_inter_closure]
+
+lemma coborder_eq_union_frontier_compl :
+    coborder s = s ∪ (frontier s)ᶜ := by
+  rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
+    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
+
+lemma coborder_eq_univ_iff :
+    coborder s = univ ↔ IsClosed s := by
+  simp [coborder, diff_eq_empty, closure_subset_iff_isClosed]
+
+alias ⟨_, IsClosed.coborder_eq⟩ := coborder_eq_univ_iff
+
+lemma coborder_eq_compl_frontier_iff :
+    coborder s = (frontier s)ᶜ ↔ IsOpen s := by
+  simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
+    disjoint_frontier_iff_isOpen]
+
+alias ⟨_, IsOpen.coborder_eq⟩ := coborder_eq_compl_frontier_iff
+
+lemma IsOpenMap.coborder_preimage_subset (hf : IsOpenMap f) (s : Set β) :
+    coborder (f ⁻¹' s) ⊆ f ⁻¹' (coborder s) := by
+  rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]
+  apply diff_subset_diff_left
+  exact hf.preimage_closure_subset_closure_preimage
+
+lemma Continuous.preimage_coborder_subset (hf : Continuous f) (s : Set β) :
+    f ⁻¹' (coborder s) ⊆ coborder (f ⁻¹' s) := by
+  rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]
+  apply diff_subset_diff_left
+  exact hf.closure_preimage_subset s
+
+lemma coborder_preimage (hf : IsOpenMap f) (hf' : Continuous f) (s : Set β) :
+    coborder (f ⁻¹' s) = f ⁻¹' (coborder s) :=
+  (hf.coborder_preimage_subset s).antisymm (hf'.preimage_coborder_subset s)
+
+protected
+lemma OpenEmbedding.coborder_preimage (hf : OpenEmbedding f) (s : Set β) :
+    coborder (f ⁻¹' s) = f ⁻¹' (coborder s) :=
+  coborder_preimage hf.isOpenMap hf.continuous s
+
+lemma isClosed_preimage_val_coborder :
+    IsClosed (coborder s ↓∩ s) := by
+  rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]
+
+/--
+A set is locally closed if it is the intersection of some open set and some closed set.
+Also see `isLocallyClosed_tfae`.
+-/
+def IsLocallyClosed (s : Set α) : Prop := ∃ (U Z : Set α), IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z
+
+lemma IsOpen.isLocallyClosed (hs : IsOpen s) : IsLocallyClosed s :=
+  ⟨_, _, hs, isClosed_univ, (inter_univ _).symm⟩
+
+lemma IsClosed.isLocallyClosed (hs : IsClosed s) : IsLocallyClosed s :=
+  ⟨_, _, isOpen_univ, hs, (univ_inter _).symm⟩
+
+lemma IsLocallyClosed.inter (hs : IsLocallyClosed s) (ht : IsLocallyClosed t) :
+    IsLocallyClosed (s ∩ t) := by
+  obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs
+  obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht
+  refine ⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩
+
+lemma IsLocallyClosed.preimage {s : Set β} (hs : IsLocallyClosed s)
+    {f : α → β} (hf : Continuous f) :
+    IsLocallyClosed (f ⁻¹' s) := by
+  obtain ⟨U, Z, hU, hZ, rfl⟩ := hs
+  exact ⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩
+
+nonrec
+lemma Inducing.isLocallyClosed_iff {s : Set α}
+    {f : α → β} (hf : Inducing f) :
+    IsLocallyClosed s ↔ ∃ s' : Set β, IsLocallyClosed s' ∧ f ⁻¹' s' = s := by
+  simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]
+  constructor
+  · rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
+    exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
+  · rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
+    exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
+
+lemma Embedding.isLocallyClosed_iff {s : Set α}
+    {f : α → β} (hf : Embedding f) :
+    IsLocallyClosed s ↔ ∃ s' : Set β, IsLocallyClosed s' ∧ s' ∩ range f = f '' s := by
+  simp_rw [hf.toInducing.isLocallyClosed_iff,
+    ← (image_injective.mpr hf.inj).eq_iff, image_preimage_eq_inter_range]
+
+lemma IsLocallyClosed.image {s : Set α} (hs : IsLocallyClosed s)
+    {f : α → β} (hf : Inducing f) (hf' : IsLocallyClosed (range f)) :
+    IsLocallyClosed (f '' s) := by
+  obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs
+  rw [image_preimage_eq_inter_range]
+  exact ht.inter hf'
+
+/--
+A set `s` is locally closed if one of the equivalent conditions below hold
+1. It is the intersection of some open set and some closed set.
+2. The coborder `(closure s \ s)ᶜ` is open.
+3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
+4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
+5. `s` is open in the closure of `s`.
+-/
+lemma isLocallyClosed_tfae (s : Set α) :
+    List.TFAE
+    [ IsLocallyClosed s,
+      IsOpen (coborder s),
+      ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
+      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s,
+      IsOpen (closure s ↓∩ s)] := by
+  tfae_have 1 → 2
+  · rintro ⟨U, Z, hU, hZ, rfl⟩
+    have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
+      nth_rw 1 [← hZ.closure_eq]
+      rw [← compl_subset_iff_union, compl_subset_compl]
+      refine frontier_subset_closure.trans (closure_mono inter_subset_right)
+    rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
+      inter_univ]
+    exact hU.union isClosed_frontier.isOpen_compl
+  tfae_have 2 → 3
+  · exact fun h x ↦ (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩)
+  tfae_have 3 → 4
+  · intro h x hx
+    obtain ⟨t, ht, ht'⟩ := h x hx
+    obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
+    rw [isClosed_preimage_val] at ht'
+    exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
+      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩
+  tfae_have 4 → 5
+  · intro H
+    choose U hxU hU e using H
+    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
+    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
+      exact e y hy ⟨hxU, x.2⟩
+    · exact (subset_iUnion₂ _ _ <| hxU x ·)
+  tfae_have 5 → 1
+  · intro H
+    convert H.isLocallyClosed.image inducing_subtype_val
+      (by simpa using isClosed_closure.isLocallyClosed)
+    simpa using subset_closure
+  tfae_finish
+
+lemma isLocallyClosed_iff_isOpen_coborder : IsLocallyClosed s ↔ IsOpen (coborder s) :=
+  (isLocallyClosed_tfae s).out 0 1
+
+alias ⟨IsLocallyClosed.isOpen_coborder, _⟩ := isLocallyClosed_iff_isOpen_coborder
+
+lemma IsLocallyClosed.isOpen_preimage_val_closure (hs : IsLocallyClosed s) :
+    IsOpen (closure s ↓∩ s) :=
+  ((isLocallyClosed_tfae s).out 0 4).mp hs
+
+open TopologicalSpace
+
+variable {ι : Type*} {U : ι → Opens β} (hU : iSup U = ⊤)
+
+theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top (s : Set β) :
+    IsLocallyClosed s ↔ ∀ i, IsLocallyClosed ((↑) ⁻¹' s : Set (U i)) := by
+  simp_rw [isLocallyClosed_iff_isOpen_coborder]
+  rw [isOpen_iff_coe_preimage_of_iSup_eq_top hU]
+  exact forall_congr' fun i ↦ by rw [(U i).isOpen.openEmbedding_subtype_val.coborder_preimage]