Grids separating a finite set of reals

A finite set C of real numbers can be separated by a bi-infinite arithmetic progression a q = t + q h, q ∈ ℤ: choose the step h smaller than the distance between any two points of C, so that each closed interval [a q, a (q + 1)] contains at most one point of C, and choose the offset t outside the countable set C - hℤ, so that no grid point lies in C (Set.Finite.exists_strictMono_notMem_subsingleton_inter_Icc).

For the critical values of a function this is a sequence of regular values whose consecutive bands each contain at most one critical value; the sublevels at these values filter the space by its critical levels.

theorem Set.Finite.exists_strictMono_notMem_subsingleton_inter_Icc {C : Set ℝ} (hC : C.Finite) : ∃ (a : ℤ → ℝ), StrictMono a ∧ Filter.Tendsto a Filter.atBot Filter.atBot ∧ Filter.Tendsto a Filter.atTop Filter.atTop ∧ (∀ (q : ℤ), a q ∉ C) ∧ ∀ (q : ℤ), (C ∩ Icc (a q) (a (q + 1))).Subsingleton

A grid separating a finite set of reals. For a finite set C ⊆ ℝ there is a strictly increasing sequence a : ℤ → ℝ, tending to -∞ and to ∞, which avoids C and whose consecutive closed intervals [a q, a (q + 1)] each contain at most one point of C.