自然數

數學敘述

在本條目的慣例中，自然數集合 N 包含 0，並包含 0 經有限次後繼所得的 1、2、3 等數。

代表公式（精確 TeX）

n\in N

成立條件

• 本條目的符號 N 明定包含 0。
• n 表示任意一個待判定是否屬於 N 的數。

符號作用域

• n — 自然數候選
• N — 自然數集合
• ∈ — 隸屬關係

直觀、定義與常見誤解

自然數提供計數與排列離散次序的基本語言。0 表示沒有對象的數量；從任一自然數取後繼，可得到下一個自然數。

不同數學傳統對 0 是否屬於自然數有不同慣例。為了和 Lean 的 Nat 及本庫後續物件一致，本條目固定採 N 包含 0；閱讀外部資料時仍應先確認該資料的定義。

自然數本身與書寫它的數字符號不同。例如十進位符號 2、二進位符號 10 可以表示同一個自然數。

常見誤解是以為所有教材對自然數是否包含 0 都有相同約定，或把數字的書寫方式與數本身混為一談。

已採用的推導導讀

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

前置知識

驗證界線

本條目是概念候選稿；研究來源不是 OCME Evidence，尚未建立計算檢查或 Lean 形式證明。

not_formalized

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

下一個義務

建立 OCME 的 N、0 與後繼到 Lean Nat 的明確語義橋，驗證後再產生內容位址化 Evidence。

同源結構化資料

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