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

• tendsto_cofinite_cocompact_iff:
• IsClosed.tendsto_coe_cofinite_iff:

## 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} [] {f : XY} :
Filter.Tendsto f Filter.cofinite () ∀ (K : Set Y), (f ⁻¹' K).Finite
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 ()
theorem isClosed_and_discrete_iff {X : Type u_1} [] {S : Set X} :
∀ (x : X), Disjoint (nhdsWithin x {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.)

def Filter.codiscrete (X : Type u_3) [] :

In any topological space, the open sets with with discrete complement form a filter.

Equations
• = { sets := {U : Set X | }, univ_sets := , sets_of_superset := , inter_sets := }
Instances For