seq_pos_lt_seq_of_lt_of_le — Mathlib

English

If f is monotone and n > 0, x0 ≤ y0, x(k+1) < f(xk), 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>0, \\; x_0 \\le y_0 \\Rightarrow (\\forall k

Lean4

theorem seq_pos_lt_seq_of_lt_of_le (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 := by
  induction n with
  | zero => exact hn.false.elim
  | succ n
    ihn =>
    suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
    cases n with
    | zero => exact h₀
    | succ n =>
      refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;> exact hk.trans n.succ.lt_succ_self

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