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

In a topological space the sets which are open with discrete complement form a filter. We formalise this as Filter.codiscrete.

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 → Set.Finite (f ⁻¹' K)

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_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.codiscrete (X : Type u_3) [TopologicalSpace X] : Filter X

In any topological space, the open sets with with discrete complement form a filter.

Equations

• Filter.codiscrete X = { sets := {U : Set X | IsOpen U ∧ DiscreteTopology ↑Uᶜ}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }