le_iterate_pos_iff — Mathlib

English

For all f,x,m and n>0, f^{[n]}(x) ≤ x + n m iff x + m ≤ f(x).

Русский

Для любых f, x, m и n>0: f^{[n]}(x) ≤ x + n m тогда и только тогда, когда x + m ≤ f(x).

LaTeX

$$$\forall f, x, m, n:\; 0 < n \Rightarrow f^{[n]}(x) \le x + n m \iff x + m \le f(x)$$$

Lean4

theorem le_iterate_pos_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : x + n * m ≤ f^[n] x ↔ x + m ≤ f x := by
  simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)

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