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