strictAnti_int_of_succ_lt — Mathlib

English

Let f: ℤ → α with α a preorder. If f(n+1) < f(n) for all n ∈ ℤ, then f is strictly antitone: for all a < b in ℤ, f(b) < f(a).

Русский

Пусть f: ℤ → α, где α — частично упорядоченное множество. Если для всех n ∈ ℤ выполняется f(n+1) < f(n), то f является строго антимонотонной: для любых a < b в ℤ выполняется f(b) < f(a).

LaTeX

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

Lean4

theorem strictAnti_int_of_succ_lt {f : ℤ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f :=
  Int.rel_of_forall_rel_succ_of_lt (· > ·) hf

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