of_mono_bounded — Mathlib

English

A monotone bounded sequence is CauSeq abs.

Русский

Монотонная ограниченная последовательность является CauSeq abs.

LaTeX

$$$IsCauSeq(abs, f) \Leftarrow (\forall n, f(n) \le a) \\text{ and } (f(n) \le f(n+1) \\text{ not needed; use proper condition})$$$

Lean4

theorem of_mono_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, |f n| ≤ a) (hnm : ∀ n ≥ m, f n ≤ f n.succ) :
    IsCauSeq abs f :=
  (of_decreasing_bounded (-f) (a := a) (m := m) (by simpa using ham) <| by simpa using hnm).of_neg

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