# 有界單調尾與上確界論證 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-monotone-sequence-convergence-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-monotone-sequence-convergence-theorem-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 對 a_n=3-2/(n+1) 證單調、有界、sup=3 及極限。 完整 n≥0 公式、嚴格 epsilon 證書；一般定理的 supremum 步驟另明示。 ## 已知條件與符號 - algebra - epsilon - supremum - definition_here - G1 — a_n=3-2/(n+1) 對全部 n≥0 定義；使用實數上確界性。 - a_n — 具體全數列 - s — 一般定理上確界 ## 規則與來源 本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。 - mko_definition · cited — 保留全稱monotonicity與相應bound。若s=sup{a_n}，s-epsilon不是upper bound給出N，之後由monotonicity控制全部tail。sup/inf未必是某一項。有限prefix不證全序列，monotone無界或bounded nonmonotone不在定理假設。 · mko-monotone-sequence-convergence-theorem - algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。 - epsilon · prerequisite — 收斂表示每個正 epsilon 有一個整數 N，使全部 n≥N 的誤差嚴格小於 epsilon；使用實數 Archimedean 性。 - supremum · prerequisite — 非空有上界實集合有上確界 s；若 epsilon>0，s-epsilon 不是上界。 - definition_here · prerequisite — 實數數列極限 L 的 epsilon 定義：每個正 epsilon 都有 N，使所有 n≥N 的 |u_n-L|0 條件：n\ge0 規則：algebra · 依賴：G1 葉節點依據：algebra 兩分母正，證每個相鄰差正；因此全序列嚴格遞增。 S02 · implies操作前 0<2/(n+1)\le2 操作後 1\le a_n<3 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 給下界 1 與適用遞增定理的上界 3。 S03 · implies操作前 \varepsilon>0,\quad N=\lfloor2/\varepsilon\rfloor+1 操作後 0<3-a_n=2/(n+1)<\varepsilon\quad(n\ge N) 條件：無 規則：epsilon · 依賴：G1, S02 葉節點依據：epsilon 全部尾端分母更大，直接證 a_n→3。 S04 · implies操作前 u<3,\quad\varepsilon=3-u>0 操作後 a_N>3-\varepsilon=u;\quad\sup\{a_n:n\ge0\}=3 條件：無 規則：supremum · 依賴：S02, S03 葉節點依據：supremum 任何小於 3 的數都不是上界，結合上界資格得到最小性。 S05 · implies操作前 (u_n)\text{ nondecreasing and bounded above},\quad s=\sup\{u_n\} 操作後 \forall\varepsilon>0\ \exists N:\ s-\varepsilon