map_lt_of_translationNumber_lt_int

English

If τ(f) < n for some integer n, then for all x, f(x) < x + n.

Русский

Если τ(f) < n для некоторого целого n, то для всех x имеет место f(x) < x + n.

LaTeX

$$$$ \\forall f, \\forall n \\in \\mathbb{Z}, \\ f\\text{.translationNumber} < n \\Rightarrow \\forall x \\in \\mathbb{R}, \\ f(x) < x + n. $$$$

Lean4

theorem map_lt_of_translationNumber_lt_int {n : ℤ} (h : τ f < n) (x : ℝ) : f x < x + n :=
  not_le.1 <| mt f.le_translationNumber_of_add_int_le <| not_le.2 h

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