seq_lt_seq_of_lt_of_le — Mathlib

English

If f is monotone and n > 0, x0 < y0, x(k+1) ≤ f(xk) and f(yk) < y(k+1) for k < n, then xn < yn.

Русский

Если f монотонна и n>0, 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_lt_of_le (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
  cases n
  exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]

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