實數

數學敘述

實數系 R 可由有理數的 Cauchy 完備化建構；每個有理數都可嵌入 R，而不同建構仍須證明彼此等價。

代表公式（精確 TeX）

x\in R

成立條件

• 採用包含有理數嵌入的實數 Cauchy 完備化語境。

符號作用域

• x — 待判定或操作的數
• R — 實數系代表記號

直觀、定義與常見誤解

每個整數與有理數都可視為實數；有限小數也可轉成精確分數，因此不是另一種獨立數系。

實數可由有理數 Cauchy 序列的等價類建構；『補入極限點』是建構直覺，不取代完備性的精確定義與證明。

本 MKO 先建立有理點在實數線上的精確表示、比較與區間語言；無理數分類、序完備性與連續性留待後續。

常見誤解是把有限小數視為無理數、把近似小數當成精確值，或只說『沒有空隙』便宣稱完備性已證明。

已採用的推導導讀

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

前置知識

• 有理數 — 本條目以有理數的嵌入與完備化建立實數入口。

驗證界線

有限個有理點的精確重算只驗證指定表示、順序與區間，不構成實數完備性或全部無理數性質的證明。

not_formalized

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

下一個義務

綁定 Mathlib Real 的 Cauchy completion、有理數嵌入、線性序與完備性聲明及版本證據。

同源結構化資料

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