English
For a monotone f: ℤ → α and x between f n and f(n+1), there is no a with f a = x.
Русский
Для монотонной f: ℤ → α и x между f n и f(n+1) не существует a с f a = x.
LaTeX
$$$\\forall f:\\mathbb{Z} \\to α,\\ Monotone f\\to \\forall n:\\mathbb{Z},\\forall x:\\alpha,\\ f n < x\\to x < f(n+1)\\to \\forall a:\\mathbb{Z},\\ f a \\neq x.$$$
Lean4
/-- If `f` is a monotone function from `ℤ` to a preorder and `x` lies between `f n` and
`f (n + 1)`, then `x` doesn't lie in the range of `f`. -/
theorem ne_of_lt_of_lt_int {f : ℤ → α} (hf : Monotone f) (n : ℤ) {x : α} (h1 : f n < x) (h2 : x < f (n + 1)) (a : ℤ) :
f a ≠ x := by
rintro rfl
exact (hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)
