English
Let f be monotone. If x0 ≤ y0, and for all k < n we have x(k+1) ≤ f(xk) and f(yk) ≤ y(k+1), then xn ≤ yn.
Русский
Пусть f монотонна, и есть две последовательности x и y such that x0 ≤ y0, для всех k < n выполняются x(k+1) ≤ f(xk) и f(yk) ≤ y(k+1). Тогда xn ≤ yn.
LaTeX
$$$\\text{Monotone}(f) \\Rightarrow (x_0 \\le y_0) \\wedge (\\forall k < n,\; x_{k+1} \\le f(x_k)) \\wedge (\\forall k < n,\; f(y_k) \\le y_{k+1}) \\Rightarrow x_n \\le y_n.$$$
Lean4
theorem seq_le_seq (hf : Monotone f) (n : ℕ) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k))
(hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n ≤ y n := by
induction n with
| zero => exact h₀
| succ n ihn =>
refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
· exact fun k hk => hx _ (hk.trans n.lt_succ_self)
· exact fun k hk => hy _ (hk.trans n.lt_succ_self)
