ne_of_lt_of_lt_int — Mathlib

English

If f: ℤ → α is antitone and f(n+1) < x < f(n), then f(a) ≠ x for all a.

Русский

Если f : ℤ → α антитонна и f(n+1) < x < f(n), то f(a) ≠ x для всех a.

LaTeX

$$$\\forall f:\\mathbb{Z} \\to α,\\ Antitone f\\to \\forall n:\\mathbb{Z},\\forall x:\\alpha,\\ f(n+1) < x\\to x < f(n)\\to \\forall a:\\mathbb{Z},\\ f a \\neq x.$$$

Lean4

/-- If `f` is an antitone function from `ℤ` to a preorder and `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_int {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 (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Похожие утверждения