A discrete intermediate value theorem #
A sequence of natural numbers that grows by at most one per step takes every value between its
value at the start and any of its later values (Nat.exists_eq_of_forall_le_add_one). Compare
SimpleGraph.Walk.mem_support_hasse_of_ge_of_le, the same fact for walks in the Hasse diagram of
a linear order.
Main results #
Nat.exists_eq_of_forall_le_add_one: the discrete intermediate value theorem.
theorem Nat.exists_eq_of_forall_le_add_one {a : ℕ → ℕ} {k T : ℕ} (h0 : a 0 ≤ k) (hT : k ≤ a T) (hstep : ∀ (t : ℕ), t < T → a (t + 1) ≤ a t + 1) :
A discrete intermediate value theorem. A sequence of natural numbers that grows by at
most one per step up to time T takes, by time T, every value between a 0 and a T.