diff --git a/Mathlib.lean b/Mathlib.lean index cff8b0883be7ae..a0b76b9000ef97 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index 474d96016322d1..c46deb83efff51 100644 --- a/Mathlib/Topology/Basic.lean +++ b/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 diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 0db6e1d7915c41..e5c1d03449ef78 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/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 diff --git a/Mathlib/Topology/LocallyClosed.lean b/Mathlib/Topology/LocallyClosed.lean new file mode 100644 index 00000000000000..341f1b8fccf4d7 --- /dev/null +++ b/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]