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

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.

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`

.)

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

## Instances For

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