Discrete subsets of euclidean spaces

Stream: Is there code for X?

[Michael Stoll]

How do I express the statement that a subset of a euclidean space (or, more generally, a topological space) is disrcete?

[Riccardo Brasca]

cc @Xavier Roblot

[Michael Stoll]

Perhaps like this?

import Mathlib.Topology.Order

def IsDiscrete {X} [TopologicalSpace X] (S : Set X) : Prop :=
  DiscreteTopology S

[Oliver Nash]

Yes, you probably want docs#DiscreteTopology

However for a subset of a topological space, there are intrinsic and extrinsic notions of discreteness. Copying my own remarks from DiscreteSubset.lean:

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`).

We have a proof that these are equivalent for closed subsets (subject to mild hypotheses satisfied by Euclidean space) in docs#IsClosed.tendsto_coe_cofinite_iff

[Kevin Buzzard]

For example the set of reciprocals of the positive integers is discrete in the sense that the induced topology is discrete, but any holomorphic function vanishing on this set must be identically zero.

[Michael Stoll]

Right, for my intended application I'll also need that the subset is closed.

[Xavier Roblot]

Yes, docs#DiscreteTopology is what is used for ℤ-lattices, see for example docs#IsZlattice or docs#Zspan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite