# Discrete subsets of topological spaces #

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 #

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

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