seq_pos_lt_seq_of_le_of_lt — Mathlib

English

In the dual setting, if x0 ≤ y0, x(k+1) ≤ f(xk) and f(yk) < y(k+1) for k < n, then xn < yn.

Русский

В двойственной постановке, если x0 ≤ y0, x(k+1) ≤ f(xk) и f(yk) < y(k+1) для k < n, то xn < yn.

LaTeX

$$$\\text{Monotone}(f) \\Rightarrow \\forall n>0, \\; x_0 \\le y_0 \\Rightarrow (\\forall k

Lean4

theorem seq_pos_lt_seq_of_le_of_lt (hf : Monotone f) {n : ℕ} (hn : 0 < 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 :=
  hf.dual.seq_pos_lt_seq_of_lt_of_le hn h₀ hy hx

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