strictMono_x — Mathlib

English

The sequence x_n(a) is strictly increasing in n: x_n < x_{n+1} for all n.

Русский

Последовательность x_n(a) строго возрастает по n: x_n < x_{n+1} для всех n.

LaTeX

$$$\\text{StrictMono}(x^{(a)})$, i.e., $x^{(a)}_n < x^{(a)}_{n+1}$ for all n.$$

Lean4

theorem strictMono_x : StrictMono (xn a1)
  | _, 0, h => absurd h <| Nat.not_lt_zero _
  | m, n + 1, h =>
    by
    have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl) fun e => by rw [e]
    simp only [xn_succ, gt_iff_lt]
    refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)
    have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
    rwa [mul_one] at t

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