seq_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, \\; x_0 < y_0 \\Rightarrow (\\forall k

Lean4

theorem seq_lt_seq_of_le_of_lt (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 :=
  hf.dual.seq_lt_seq_of_lt_of_le n h₀ hy hx

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