iterate_lt_nfp — Mathlib

English

If f is strictly monotone and a < f(a), then every iterate f^[n] a is strictly below nfp f a.

Русский

Если f строго монотонна и a < f(a), то каждый итерат f^[n] a строго меньше nfp f a.

LaTeX

$$$$ \text{If } \text{StrictMono}(f) \text{ and } a < f(a), \ \forall n,\ f^{[n]} a < nfp f a. $$$$

Lean4

theorem iterate_lt_nfp (hf : StrictMono f) {a} (h : a < f a) (n : ℕ) : f^[n] a < nfp f a :=
  by
  apply (hf.iterate n h).trans_le
  rw [← iterate_succ_apply]
  exact iterate_le_nfp ..

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