English
If f: ℕ → α is monotone and there exists x with f(n) < x < f(n+1), then x is not in the image of f.
Русский
Если f : ℕ → α монотонна и существует x such that f(n) < x < f(n+1), то x не принадлежит образу f.
LaTeX
$$$\\forall f:\\mathbb{N} \\to α,\\ Monotone f\\to \\forall n:\\mathbb{N},\\forall x:\\alpha,\\ f(n) < x\\to x < f(n+1)\\to \\forall a:\\mathbb{N},\\ f(a) \\neq x.$$$
Lean4
/-- If `f` is a monotone function from `ℕ` to a preorder such that `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_nat {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 (Nat.le_of_lt_succ <| hf.reflect_lt h2)
