Locally closed sets

In this file, we develop API for the predicates IsLocallyClosedAt, expressing that a set is locally closed at a point, and IsLocallyClosed, expressing that a set is locally closed. These are defined earlier, but most of their API should be in this file.

Main results

• isLocallyClosedAt_tfae: A set s is locally closed at a point x if one of the equivalent conditions below hold
  1. There is a neighborhood U of x such that U ∩ s can be written U ∩ Z for some closed set Z (this is the definition).
  2. There is a neighborhood U of x such that U ∩ s is a closed subset of U.
  3. There is a neighborhood U of x such that U ∩ closure s ⊆ s.
  4. There is a neighborhood U of x such that U ∩ s = U ∩ closure s.
  5. s coincides with some closed set Z eventually near x.
  6. s and closure s coincide eventually near x.
  7. closure s ⊆ s eventually near x.
  8. s is a neighborhood of x inside closure s.
  9. coborder s is a neighborhood of x.
• 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 (this is the definition).
  2. It is locally closed at each of its points.
  3. It is locally closed at each point of its coborder.
  4. The coborder (closure s \ s)ᶜ is open.
  5. s is the intersection of an open set and closure s.
  6. s is open in the closure of s.

theorem mem_coborder_iff_imp {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : x ∈ coborder s ↔ x ∈ closure s → x ∈ s

theorem subset_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : s ⊆ coborder s

theorem coborder_inter_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s ∩ closure s = s

theorem closure_inter_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : closure s ∩ coborder s = s

theorem coborder_eq_union_frontier_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = s ∪ (frontier s)ᶜ

theorem coborder_eq_univ_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = Set.univ ↔ IsClosed s

theorem IsClosed.coborder_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed s → coborder s = Set.univ

Alias of the reverse direction of coborder_eq_univ_iff.

theorem coborder_eq_compl_frontier_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = (frontier s)ᶜ ↔ IsOpen s

theorem coborder_eq_union_closure_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = s ∪ (closure s)ᶜ

theorem dense_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : Dense (coborder s)

The coborder of any set is dense

theorem IsOpen.coborder_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen s → coborder s = (frontier s)ᶜ

Alias of the reverse direction of coborder_eq_compl_frontier_iff.

theorem IsOpenMap.coborder_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenMap f) (s : Set Y) : coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s

theorem Continuous.preimage_coborder_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (s : Set Y) : f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)

theorem coborder_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenMap f) (hf' : Continuous f) (s : Set Y) : coborder (f ⁻¹' s) = f ⁻¹' coborder s

theorem Topology.IsOpenEmbedding.coborder_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) (s : Set Y) : coborder (f ⁻¹' s) = f ⁻¹' coborder s

theorem isClosed_preimage_val_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed (Subtype.val ⁻¹' s)

theorem IsLocallyClosedAt.of_mem_nhds {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} (hx : s ∈ nhds x) : IsLocallyClosedAt s x

theorem IsLocallyClosedAt.of_notMem_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} (hx : x ∉ closure s) : IsLocallyClosedAt s x

theorem IsLocallyClosedAt.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {s : Set Y} {f : X → Y} (hs : IsLocallyClosedAt s (f x)) (hf : Continuous f) : IsLocallyClosedAt (f ⁻¹' s) x

theorem isLocallyClosedAt_tfae {X : Type u_1} [TopologicalSpace X] (s : Set X) (x : X) : [IsLocallyClosedAt s x, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s), ∃ U ∈ nhds x, U ∩ closure s ⊆ s, ∃ U ∈ nhds x, U ∩ s = U ∩ closure s, ∃ (Z : Set X), IsClosed Z ∧ s =ᶠ[nhds x] Z, s =ᶠ[nhds x] closure s, closure s ≤ᶠ[nhds x] s, s ∈ nhdsWithin x (closure s), coborder s ∈ nhds x].TFAE

A set s is locally closed at a point x if one of the equivalent conditions below hold

1. There is a neighborhood U of x such that U ∩ s can be written U ∩ Z for some closed set Z (this is the definition).
2. There is a neighborhood U of x such that U ∩ s is a closed subset of U.
3. There is a neighborhood U of x such that U ∩ closure s ⊆ s.
4. There is a neighborhood U of x such that U ∩ s = U ∩ closure s.
5. s coincides with some closed set Z eventually near x.
6. s and closure s coincide eventually near x.
7. closure s ⊆ s eventually near x.
8. s is a neighborhood of x inside closure s.
9. coborder s is a neighborhood of x.

Furthermore (see API below), in assertions 1, 2, 3 and 4, one can restrict to U belonging to a basis of neighborhoods of x.

theorem isLocallyClosedAt_iff_exists_isClosed_preimage_val {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s)

theorem isLocallyClosedAt_iff_exists_inter_closure_subset {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ ∃ U ∈ nhds x, U ∩ closure s ⊆ s

theorem isLocallyClosedAt_iff_exists_eq_inter_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ ∃ U ∈ nhds x, U ∩ s = U ∩ closure s

theorem isLocallyClosedAt_iff_exists_isClosed_inter_eq_of_hasBasis {X : Type u_1} [TopologicalSpace X] {s : Set X} {ι : Type u_3} {p : ι → Prop} {U : ι → Set X} {x : X} (H : (nhds x).HasBasis p U) : IsLocallyClosedAt s x ↔ ∃ (i : ι), p i ∧ ∃ (Z : Set X), IsClosed Z ∧ U i ∩ s = U i ∩ Z

theorem isLocallyClosedAt_iff_exists_isClosed_preimage_val_of_hasBasis {X : Type u_1} [TopologicalSpace X] {s : Set X} {ι : Type u_3} {p : ι → Prop} {U : ι → Set X} {x : X} (H : (nhds x).HasBasis p U) : IsLocallyClosedAt s x ↔ ∃ (i : ι), p i ∧ IsClosed (Subtype.val ⁻¹' s)

theorem isLocallyClosedAt_iff_exists_inter_closure_subset_of_hasBasis {X : Type u_1} [TopologicalSpace X] {s : Set X} {ι : Type u_3} {p : ι → Prop} {U : ι → Set X} {x : X} (H : (nhds x).HasBasis p U) : IsLocallyClosedAt s x ↔ ∃ (i : ι), p i ∧ U i ∩ closure s ⊆ s

theorem isLocallyClosedAt_iff_exists_eq_inter_closure_of_hasBasis {X : Type u_1} [TopologicalSpace X] {s : Set X} {ι : Type u_3} {p : ι → Prop} {U : ι → Set X} {x : X} (H : (nhds x).HasBasis p U) : IsLocallyClosedAt s x ↔ ∃ (i : ι), p i ∧ U i ∩ s = U i ∩ closure s

theorem isLocallyClosedAt_iff_exists_isClosed_eventuallyEqSet {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ ∃ (Z : Set X), IsClosed Z ∧ s =ᶠ[nhds x] Z

@[deprecated isLocallyClosedAt_iff_exists_isClosed_eventuallyEqSet (since := "2026-09-02")]

theorem isLocallyClosedAt_iff_exists_isClosed_eventuallyEq {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ ∃ (Z : Set X), IsClosed Z ∧ s =ᶠ[nhds x] Z

Alias of isLocallyClosedAt_iff_exists_isClosed_eventuallyEqSet.

theorem isLocallyClosedAt_iff_eventuallyEqSet_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ s =ᶠ[nhds x] closure s

@[deprecated isLocallyClosedAt_iff_eventuallyEqSet_closure (since := "2026-09-02")]

theorem isLocallyClosedAt_iff_eventuallyEq_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ s =ᶠ[nhds x] closure s

Alias of isLocallyClosedAt_iff_eventuallyEqSet_closure.

theorem isLocallyClosedAt_iff_closure_eventuallySubset {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ closure s ≤ᶠ[nhds x] s

@[deprecated isLocallyClosedAt_iff_closure_eventuallySubset (since := "2026-09-02")]

theorem isLocallyClosedAt_iff_closure_eventuallyLE {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ closure s ≤ᶠ[nhds x] s

Alias of isLocallyClosedAt_iff_closure_eventuallySubset.

theorem isLocallyClosedAt_iff_coborder_mem_nhds {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsLocallyClosedAt s x ↔ coborder s ∈ nhds x

theorem IsLocallyClosedAt.congr {X : Type u_1} [TopologicalSpace X] {s t : Set X} {x : X} (hs : IsLocallyClosedAt s x) (h : s =ᶠ[nhds x] t) : IsLocallyClosedAt t x

theorem isLocallyClosedAt_congr {X : Type u_1} [TopologicalSpace X] {s t : Set X} {x : X} (h : s =ᶠ[nhds x] t) : IsLocallyClosedAt s x ↔ IsLocallyClosedAt t x

theorem interior_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : interior (coborder s) = {x : X | IsLocallyClosedAt s x}

theorem IsLocallyClosedAt.inter {X : Type u_1} [TopologicalSpace X] {s t : Set X} {x : X} (hs : IsLocallyClosedAt s x) (ht : IsLocallyClosedAt t x) : IsLocallyClosedAt (s ∩ t) x

theorem IsLocallyClosedAt.union {X : Type u_1} [TopologicalSpace X] {s t : Set X} {x : X} (hs : IsLocallyClosedAt s x) (ht : IsLocallyClosedAt t x) : IsLocallyClosedAt (s ∪ t) x

theorem IsLocallyClosed.isLocallyClosedAt {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsLocallyClosed s) {x : X} (hx : x ∈ s) : IsLocallyClosedAt s x

theorem IsLocallyClosed.inter {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsLocallyClosed s) (ht : IsLocallyClosed t) : IsLocallyClosed (s ∩ t)

theorem IsLocallyClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (hs : IsLocallyClosed s) {f : X → Y} (hf : Continuous f) : IsLocallyClosed (f ⁻¹' s)

theorem Topology.IsInducing.isLocallyClosed_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : IsInducing f) : IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = s

theorem Topology.IsEmbedding.isLocallyClosed_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : IsEmbedding f) : IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ Set.range f = f '' s

theorem IsLocallyClosed.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsLocallyClosed s) {f : X → Y} (hf : Topology.IsInducing f) (hf' : IsLocallyClosed (Set.range f)) : IsLocallyClosed (f '' s)

theorem isLocallyClosed_tfae {X : Type u_1} [TopologicalSpace X] (s : Set X) : [IsLocallyClosed s, ∀ x ∈ s, IsLocallyClosedAt s x, ∀ x ∈ coborder s, IsLocallyClosedAt s x, IsOpen (coborder s), ∃ (U : Set X), IsOpen U ∧ s = U ∩ closure s, IsOpen (Subtype.val ⁻¹' s)].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 (this is the definition).
2. It is locally closed at each of its points.
3. It is locally closed at each point of its coborder.
4. The coborder (closure s \ s)ᶜ is open.
5. s is the intersection of an open set and closure s.
6. s is open in the closure of s.

theorem isLocallyClosed_iff_isLocallyClosedAt {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsLocallyClosed s ↔ ∀ x ∈ s, IsLocallyClosedAt s x

theorem isLocallyClosed_iff_isOpen_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsLocallyClosed s ↔ IsOpen (coborder s)

theorem IsLocallyClosed.isOpen_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsLocallyClosed s → IsOpen (coborder s)

Alias of the forward direction of isLocallyClosed_iff_isOpen_coborder.

theorem isLocallyClosed_iff_isOpen_preimage_val_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsLocallyClosed s ↔ IsOpen (Subtype.val ⁻¹' s)

theorem IsLocallyClosed.isOpen_preimage_val_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsLocallyClosed s → IsOpen (Subtype.val ⁻¹' s)

Alias of the forward direction of isLocallyClosed_iff_isOpen_preimage_val_closure.