le_iterate_of_add_int_le_map — Mathlib

English

If x + m ≤ f x, then for all n, x + n m ≤ f^{[n]}(x).

Русский

Если x + m ≤ f(x), то для всех n выполняется x + n m ≤ f^{[n]}(x).

LaTeX

$$$\forall x\in \mathbb{R}, \forall m\in \mathbb{Z},\; x + m \le f(x) \Rightarrow \forall n\in \mathbb{N},\; x + n m \le f^{[n]}(x)$$$

Lean4

theorem le_iterate_of_add_int_le_map {x : ℝ} {m : ℤ} (h : x + m ≤ f x) (n : ℕ) : x + n * m ≤ f^[n] x := by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).symm.iterate_le_of_map_le (monotone_id.add_const (m : ℝ)) f.monotone h n

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