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 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 Y] {f : X → Y} [TopologicalSpace X] [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 Y] {f : X → Y} [TopologicalSpace X] [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_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)

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

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

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

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

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.

@[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.

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.

Equations

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

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