# Discrete subsets of topological spaces #

This file contains various additional properties of discrete subsets of topological spaces.

## Discreteness and compact sets #

Given a topological space `X` together with a subset `s ⊆ X`, there are two distinct concepts of "discreteness" which may hold. These are: (i) Every point of `s` is isolated (i.e., the subset topology induced on `s` is the discrete topology). (ii) Every compact subset of `X` meets `s` only finitely often (i.e., the inclusion map `s → X` tends to the cocompact filter along the cofinite filter on `s`).

When `s` is closed, the two conditions are equivalent provided `X` is locally compact and T1, see `IsClosed.tendsto_coe_cofinite_iff`.

### Main statements #

- `tendsto_cofinite_cocompact_iff`:
- `IsClosed.tendsto_coe_cofinite_iff`:

## Co-discrete open sets #

We define the filter `Filter.codiscreteWithin S`, which is the supremum of all `𝓝[S \ {x}] x`. This is the filter of all open codiscrete sets within S. We also define `Filter.codiscrete` as `Filter.codiscreteWithin univ`, which is the filter of all open codiscrete sets in the space.

source
theorem discreteTopology_subtype_iff {Y : Type u_2} [TopologicalSpace Y] {S : Set Y} :
DiscreteTopology ↑S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥
source
theorem discreteTopology_subtype_iff' {Y : Type u_2} [TopologicalSpace Y] {S : Set Y} :
DiscreteTopology ↑S ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen U ∧ U ∩ S = {y}
source
theorem tendsto_cofinite_cocompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {f : X → Y} :
Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
source
theorem Continuous.discrete_of_tendsto_cofinite_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T1Space X] [WeaklyLocallyCompactSpace Y] (hf' : Continuous f) (hf : Filter.Tendsto f Filter.cofinite (Filter.cocompact Y)) :
DiscreteTopology X
source
theorem tendsto_cofinite_cocompact_of_discrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [DiscreteTopology X] (hf : Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)) :
Filter.Tendsto f Filter.cofinite (Filter.cocompact Y)
source
theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) (_hs' : DiscreteTopology ↑s) :
Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)
source
theorem IsClosed.tendsto_coe_cofinite_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] [WeaklyLocallyCompactSpace X] {s : Set X} (hs : IsClosed s) :
Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X) ↔ DiscreteTopology ↑s
source
theorem isClosed_and_discrete_iff {X : Type u_1} [TopologicalSpace X] {S : Set X} :
IsClosed S ∧ DiscreteTopology ↑S ↔ ∀ (x : X), Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal S)

Criterion for a subset `S ⊆ X` to be closed and discrete in terms of the punctured neighbourhood filter at an arbitrary point of `X`. (Compare `discreteTopology_subtype_iff`.)

source
def Filter.codiscreteWithin {X : Type u_1} [TopologicalSpace X] (S : Set X) :
Filter X

The filter of sets with no accumulation points inside a set `S : Set X`, implemented as the supremum over all punctured neighborhoods within `S`.

Equations

- Filter.codiscreteWithin S = ⨆ x ∈ S, nhdsWithin x (S \ {x})

Instances For

source
theorem mem_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {S T : Set X} :
S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal (T \ S))
source
theorem mem_codiscreteWithin_iff_forall_mem_nhdsNE {X : Type u_1} [TopologicalSpace X] {S T : Set X} :
S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, S ∪ T ᶜ ∈ nhdsWithin x {x}ᶜ

A set `s` is codiscrete within `U` iff `s ∪ Uᶜ` is a punctured neighborhood of every point in `U`.

source
theorem mem_codiscreteWithin_accPt {X : Type u_1} [TopologicalSpace X] {S T : Set X} :
S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (Filter.principal (T \ S))
source
@[simp]
theorem Filter.self_mem_codiscreteWithin {X : Type u_1} [TopologicalSpace X] (U : Set X) :
U ∈ codiscreteWithin U

Any set is codiscrete within itself.

source
theorem Filter.codiscreteWithin.mono {X : Type u_1} [TopologicalSpace X] {U₁ U : Set X} (hU : U₁ ⊆ U) :
codiscreteWithin U₁ ≤ codiscreteWithin U

If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`.

source
theorem discreteTopology_of_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {U s : Set X} (h : s ∈ Filter.codiscreteWithin U) :
DiscreteTopology ↑(s ᶜ ∩ U)

If `s` is codiscrete within `U`, then `sᶜ ∩ U` has discrete topology.

source
theorem codiscreteWithin_iff_locallyEmptyComplementWithin {X : Type u_1} [TopologicalSpace X] {s U : Set X} :
s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhdsWithin z {z}ᶜ, t ∩ (U \ s) = ∅

Helper lemma for `codiscreteWithin_iff_locallyFiniteComplementWithin`: A set `s` is `codiscreteWithin U` iff every point `z ∈ U` has a punctured neighborhood that does not intersect `U \ s`.

source
theorem isClosed_sdiff_of_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {s U : Set X} (hs : s ∈ Filter.codiscreteWithin U) (hU : IsClosed U) :
IsClosed (U \ s)

If `U` is closed and `s` is codiscrete within `U`, then `U \ s` is closed.

source
theorem nhdsNE_of_nhdsNE_sdiff_finite {X : Type u_3} [TopologicalSpace X] [T1Space X] {x : X} {U s : Set X} (hU : U ∈ nhdsWithin x {x}ᶜ) (hs : Finite ↑s) :
U \ s ∈ nhdsWithin x {x}ᶜ

In a T1Space, punctured neighborhoods are stable under removing finite sets of points.

source
@[deprecated nhdsNE_of_nhdsNE_sdiff_finite (since := "2025-05-22")]
theorem nhdNE_of_nhdNE_sdiff_finite {X : Type u_3} [TopologicalSpace X] [T1Space X] {x : X} {U s : Set X} (hU : U ∈ nhdsWithin x {x}ᶜ) (hs : Finite ↑s) :
U \ s ∈ nhdsWithin x {x}ᶜ

Alias of `nhdsNE_of_nhdsNE_sdiff_finite`.

In a T1Space, punctured neighborhoods are stable under removing finite sets of points.

source
theorem codiscreteWithin_iff_locallyFiniteComplementWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {s U : Set X} :
s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ (U \ s)).Finite

In a T1Space, a set `s` is codiscreteWithin `U` iff it has locally finite complement within `U`. More precisely: `s` is codiscreteWithin `U` iff every point `z ∈ U` has a punctured neighborhood intersect `U \ s` in only finitely many points.

source
def Filter.codiscrete (X : Type u_3) [TopologicalSpace X] :
Filter X

In any topological space, the open sets with discrete complement form a filter, defined as the supremum of all punctured neighborhoods.

See `Filter.mem_codiscrete'` for the equivalence.

Equations

- Filter.codiscrete X = Filter.codiscreteWithin Set.univ

Instances For

source
theorem mem_codiscrete {X : Type u_1} [TopologicalSpace X] {S : Set X} :
S ∈ Filter.codiscrete X ↔ ∀ (x : X), Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal S ᶜ)
source
theorem mem_codiscrete_accPt {X : Type u_1} [TopologicalSpace X] {S : Set X} :
S ∈ Filter.codiscrete X ↔ ∀ (x : X), ¬AccPt x (Filter.principal S ᶜ)
source
theorem mem_codiscrete' {X : Type u_1} [TopologicalSpace X] {S : Set X} :
S ∈ Filter.codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑S ᶜ
source
theorem mem_codiscrete_subtype_iff_mem_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {S : Set X} {U : Set ↑S} :
U ∈ Filter.codiscrete ↑S ↔ Subtype.val '' U ∈ Filter.codiscreteWithin S
source
theorem compl_mem_codiscrete_iff {X : Type u_1} [TopologicalSpace X] {S : Set X} :
S ᶜ ∈ Filter.codiscrete X ↔ IsClosed S ∧ DiscreteTopology ↑S
source
theorem discreteTopology_union {X : Type u_1} [TopologicalSpace X] {S T : Set X} (hs : DiscreteTopology ↑S) (ht : DiscreteTopology ↑T) (hs' : IsClosed S) (ht' : IsClosed T) :
DiscreteTopology ↑(S ∪ T)

The union of two discrete closed subsets is discrete.

source
theorem discreteTopology_biUnion_finset {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {I : Finset ι} {s : ι → Set X} (hs : ∀ i ∈ I, DiscreteTopology ↑(s i)) (hs' : ∀ i ∈ I, IsClosed (s i)) :
DiscreteTopology ↑(⋃ i ∈ I, s i)

The union of finitely many discrete closed subsets is discrete.

source
theorem discreteTopology_iUnion_fintype {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} [Fintype ι] {s : ι → Set X} (hs : ∀ (i : ι), DiscreteTopology ↑(s i)) (hs' : ∀ (i : ι), IsClosed (s i)) :
DiscreteTopology ↑(⋃ (i : ι), s i)

The union of finitely many discrete closed subsets is discrete.