English
If f: ℕ → α is antitone and there is x with f(n+1) < x < f(n), then f(a) ≠ x for all a.
Русский
Если f : ℕ → α антитонна и найдется x с f(n+1) < x < f(n), то f(a) ≠ x для всех a.
LaTeX
$$$\\forall f:\\mathbb{N} \\to α,\\ Antitone f\\to \\forall n:\\mathbb{N},\\forall x:\\alpha,\\ f(n+1) < x\\to x < f(n)\\to \\forall a:\\mathbb{N},\\ f(a) \\neq x.$$$
Lean4
/-- If `f` is an antitone function from `ℕ` to a preorder such that `x` lies between `f (n + 1)` and
`f n`, then `x` doesn't lie in the range of `f`. -/
theorem ne_of_lt_of_lt_nat {f : ℕ → α} (hf : Antitone f) (n : ℕ) {x : α} (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℕ) :
f a ≠ x := by
rintro rfl
exact (hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)
