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_accPt {X : Type u_1} [TopologicalSpace X] {S T : Set X} : S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (Filter.principal (T \ S))

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