Discrete intermediate values #
A sequence in a linearly ordered successor order that increases by at most one successor at each step attains every value between its initial and final values. Downward jumps and repeated values are allowed. The step bound is needed only on the finite interval in question.
This separates finite level crossing from the limit argument in
TauCeti.map_atTop_eq_of_le_add_one: a sequence tending to infinity with eventually bounded
upward steps takes every sufficiently large natural value.
theorem
Nat.exists_mem_Icc_eq_of_le_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{f : ℕ → α}
{a b : ℕ}
{y : α}
(hab : a ≤ b)
(hstep : ∀ (i : ℕ), a ≤ i → i < b → f (i + 1) ≤ Order.succ (f i))
(ha : f a ≤ y)
(hb : y ≤ f b)
:
Discrete intermediate value theorem. If a sequence increases by at most one successor
at each step between a and b, then it attains every value between f a and f b at an index
in [a, b]. No restriction is imposed on downward jumps.