iterate_le_of_map_le_add_int — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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