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.

def coborder {X : Type u_1} [TopologicalSpace X] (s : Set X) : Set X

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.

Equations

• coborder s = (closure s \ 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 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 OpenEmbedding.coborder_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : OpenEmbedding 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)

def IsLocallyClosed {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A set is locally closed if it is the intersection of some open set and some closed set. Also see isLocallyClosed_tfae.

Equations

• IsLocallyClosed s = ∃ (U : Set X) (Z : Set X), IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z

theorem IsOpen.isLocallyClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : IsLocallyClosed s

theorem IsClosed.isLocallyClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : IsLocallyClosed s

theorem IsLocallyClosed.inter {X : Type u_1} [TopologicalSpace X] {s : Set X} {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 Inducing.isLocallyClosed_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Inducing f) : IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = s

theorem Embedding.isLocallyClosed_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Embedding 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 : Inducing f) (hf' : IsLocallyClosed (Set.range f)) : IsLocallyClosed (f '' s)

theorem isLocallyClosed_tfae {X : Type u_1} [TopologicalSpace X] (s : Set X) : [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s), ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ 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.
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.

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.isOpen_preimage_val_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsLocallyClosed s) : IsOpen (Subtype.val ⁻¹' s)

theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_3} {U : ι → TopologicalSpace.Opens Y} (hU : iSup U = ⊤) (s : Set Y) : IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)