數列

數學敘述

在 N={0,1,2,…} 的慣例下，實數數列為函數 a:N→R，第 n 項記為 a(n) 或 a_n。有限數列則明示長度 L 及索引 {0,…,L-1}。

代表公式（精確 TeX）

a:N\to R

成立條件

• 無限數列採 N 包含 0，並把 a_0 稱為起始項。
• 有限數列的長度 L 為非負整數，只有 0≤n<L 可用；遞迴規則須附初始條件。

符號作用域

• a — 實數數列
• N — 包含 0 的自然數索引
• R — 實數陪域

直觀、定義與常見誤解

數列的相同數值可以出現在不同索引；索引次序是函數資料的一部分，與無序集合不同。

通項式直接指定 a_n；遞迴式以初始條件及先前項指定後續項。本轮有限計算用明示 a_n=u+dn 或 a_0=u、a_(n+1)=a_n+d。

只有幾個初始項通常不能唯一推定後續規則。數列極限、單調性、無窮級數與一般遞迴存在唯一性保留為後續。

混淆從 0 或 1 起始的索引，或僅憑一段前綴宣稱已找出唯一數列。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 函數映射 — 數列依索引為每個位置指定唯一項。
• 自然數 — 自然數索引從 0 起始。
• 實數 — 本輪數列的陪域限定為實數。

驗證界線

指定公式与遞迴的有限項可精確重算；沒有宣稱數列收斂或无窮性質已證明。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

綁定 Nat→Real、Fin L 有限索引與附初值遞迴的精確語義。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。