A discrete intermediate value theorem

An integer-valued sequence whose consecutive terms differ by at most 1 attains every integer value lying between two of its terms. This is the discrete analogue of the intermediate value theorem for a unit-step walk on ℤ.

theorem Int.exists_eq_of_natAbs_sub_le_one (f : ℕ → ℤ) (hf : ∀ (n : ℕ), (f (n + 1) - f n).natAbs ≤ 1) {a b : ℕ} (hab : a ≤ b) {t : ℤ} (hta : f a ≤ t) (htb : t ≤ f b) : ∃ (c : ℕ), a ≤ c ∧ c ≤ b ∧ f c = t

Discrete intermediate value theorem. If an integer-valued sequence f : ℕ → ℤ has consecutive terms differing by at most 1, then it attains every value between f a and f b: for a ≤ b and f a ≤ t ≤ f b there is some index c ∈ [a, b] with f c = t.