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.

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 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

@[deprecated IsOpenEmbedding.coborder_preimage]

theorem OpenEmbedding.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

Alias of IsOpenEmbedding.coborder_preimage.

theorem isClosed_preimage_val_coborder {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed (Subtype.val ⁻¹' 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 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

@[deprecated IsInducing.isLocallyClosed_iff]

theorem Inducing.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

Alias of IsInducing.isLocallyClosed_iff.

theorem 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

@[deprecated IsEmbedding.isLocallyClosed_iff]

theorem Embedding.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

Alias of IsEmbedding.isLocallyClosed_iff.

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 : IsInducing 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)