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 : XY} :
Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) ∀ (K : Set Y), IsCompact KSet.Finite (f ⁻¹' K)
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)