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.

theorem discreteTopology_subtype_iff {Y : Type u_2} [TopologicalSpace Y] {S : Set Y} : DiscreteTopology ↑S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥

theorem isDiscrete_iff_nhdsNE {Y : Type u_2} [TopologicalSpace Y] {S : Set Y} : IsDiscrete S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥

theorem discreteTopology_of_noAccPts {X : Type u_3} [TopologicalSpace X] {E : Set X} (h : ∀ x ∈ E, ¬AccPt x (Filter.principal E)) : DiscreteTopology ↑E

If a subset of a topological space has no accumulation points, then it carries the discrete topology.

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}

theorem isDiscrete_iff_forall_exists_isOpen {Y : Type u_2} [TopologicalSpace Y] {S : Set Y} : IsDiscrete S ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen U ∧ U ∩ S = {y}

theorem Set.Subsingleton.isDiscrete {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : s.Subsingleton) : IsDiscrete s

theorem isDiscrete_iff_nhdsWithin {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsDiscrete s ↔ ∀ x ∈ s, nhdsWithin x s = pure x

theorem IsDiscrete.nhdsWithin {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsDiscrete s → ∀ x ∈ s, nhdsWithin x s = pure x

Alias of the forward direction of isDiscrete_iff_nhdsWithin.

theorem IsDiscrete.of_nhdsWithin {X : Type u_1} [TopologicalSpace X] {s : Set X} (H : ∀ x ∈ s, nhdsWithin x s ≤ pure x) : IsDiscrete s

theorem isDiscrete_univ_iff {X : Type u_1} [TopologicalSpace X] : IsDiscrete Set.univ ↔ DiscreteTopology X

theorem IsDiscrete.univ {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : IsDiscrete Set.univ

theorem IsDiscrete.image_of_isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hs : IsDiscrete s) (hf : IsOpenMap f) (hf' : Function.Injective f) : IsDiscrete (f '' s)

theorem IsDiscrete.image_of_isOpenMap_of_isOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hs : IsDiscrete s) (hf : IsOpenMap f) (hs' : IsOpen s) : IsDiscrete (f '' s)

theorem IsOpenMap.isDiscrete_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [DiscreteTopology X] (hf : IsOpenMap f) : IsDiscrete (Set.range f)

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

theorem IsInducing.isDiscrete_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [DiscreteTopology X] (hf : Topology.IsInducing f) : IsDiscrete (Set.range f)

@[deprecated IsInducing.isDiscrete_range (since := "2026-03-30")]

theorem IsEmbedding.isDiscrete_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [DiscreteTopology X] (hf : Topology.IsInducing f) : IsDiscrete (Set.range f)

Alias of IsInducing.isDiscrete_range.

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

theorem IsDiscrete.preimage' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : IsDiscrete s) (hf : ContinuousOn f (f ⁻¹' s)) (H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})) : IsDiscrete (f ⁻¹' s)

If f is continuous with discrete fibers, then the preimage of discrete sets are discrete.

theorem IsDiscrete.eq_of_specializes {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsDiscrete s) {a b : X} (hab : a ⤳ b) (ha : a ∈ s) (hb : b ∈ s) : a = b

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

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

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)

theorem IsClosed.tendsto_coe_cofinite_of_isDiscrete {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) (hs' : IsDiscrete s) : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)

@[deprecated IsClosed.tendsto_coe_cofinite_of_isDiscrete (since := "2025-10-08")]

theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) (hs' : IsDiscrete s) : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)

Alias of IsClosed.tendsto_coe_cofinite_of_isDiscrete.

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) ↔ IsDiscrete s

theorem isClosed_and_discrete_iff {X : Type u_1} [TopologicalSpace X] {S : Set X} : IsClosed S ∧ IsDiscrete 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 isDiscrete_iff_nhds_ne.)

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.

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

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.

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

@[simp]

theorem Filter.self_mem_codiscreteWithin {X : Type u_1} [TopologicalSpace X] (U : Set X) : U ∈ codiscreteWithin U

Any set is codiscrete within itself.

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.

theorem isDiscrete_of_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {U s : Set X} (h : sᶜ ∈ Filter.codiscreteWithin U) : IsDiscrete (s ∩ U)

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

@[deprecated isDiscrete_of_codiscreteWithin (since := "2025-10-08")]

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

Alias of isDiscrete_of_codiscreteWithin.

---

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

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.

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.

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.

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.

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.

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

theorem mem_codiscrete_accPt {X : Type u_1} [TopologicalSpace X] {S : Set X} : S ∈ Filter.codiscrete X ↔ ∀ (x : X), ¬AccPt x (Filter.principal Sᶜ)

theorem mem_codiscrete' {X : Type u_1} [TopologicalSpace X] {S : Set X} : S ∈ Filter.codiscrete X ↔ IsOpen S ∧ IsDiscrete Sᶜ

theorem compl_mem_codiscrete_iff {X : Type u_1} [TopologicalSpace X] {S : Set X} : Sᶜ ∈ Filter.codiscrete X ↔ IsClosed S ∧ DiscreteTopology ↑S

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

theorem codiscrete_le_cofinite {X : Type u_1} [TopologicalSpace X] [T1Space X] : Filter.codiscrete X ≤ Filter.cofinite

theorem Set.Finite.compl_mem_codiscrete {X : Type u_1} [TopologicalSpace X] [T1Space X] {S : Set X} (hs : S.Finite) : Sᶜ ∈ Filter.codiscrete X

theorem Set.Infinite.of_accPt {X : Type u_1} [TopologicalSpace X] [T1Space X] {S : Set X} {x : X} (h : AccPt x (Filter.principal S)) : S.Infinite

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.

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.

theorem discreteTopology_iUnion_finite {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} [Finite ι] {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.

@[deprecated discreteTopology_iUnion_finite (since := "2025-11-28")]

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

Alias of discreteTopology_iUnion_finite.

---

The union of finitely many discrete closed subsets is discrete.