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 #
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
.
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
.)
In any topological space, the open sets with with discrete complement form a filter.
Equations
- One or more equations did not get rendered due to their size.