# 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

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