# Documentation

Mathlib.Topology.DiscreteSubset

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

• tendsto_cofinite_cocompact_iff:
• IsClosed.tendsto_coe_cofinite_iff:
theorem tendsto_cofinite_cocompact_iff {X : Type u_1} {Y : Type u_2} [] {f : XY} :
Filter.Tendsto f Filter.cofinite () ∀ (K : Set Y), Set.Finite (f ⁻¹' K)
theorem Continuous.discrete_of_tendsto_cofinite_cocompact {X : Type u_1} {Y : Type u_2} [] [] {f : XY} [] (hf' : ) (hf : Filter.Tendsto f Filter.cofinite ()) :
theorem tendsto_cofinite_cocompact_of_discrete {X : Type u_1} {Y : Type u_2} [] [] {f : XY} [] (hf : ) :
Filter.Tendsto f Filter.cofinite ()
theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology {X : Type u_1} [] {s : Set X} (hs : ) (_hs' : ) :
Filter.Tendsto Subtype.val Filter.cofinite ()
theorem IsClosed.tendsto_coe_cofinite_iff {X : Type u_1} [] [] {s : Set X} (hs : ) :
Filter.Tendsto Subtype.val Filter.cofinite ()