Documentation

Mathlib.Topology.DiscreteSubset

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.

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 K(f ⁻¹' K).Finite
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)

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
Instances For