# 實數

實數包含有理數，並以完備化補入有理數系統中缺少的極限點。

mko-real-number · concept · v0.10.0



## 數學敘述

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





## 代表公式（精確 TeX）

x\in R





## 成立條件


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





## 符號作用域


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





## 直觀、定義與常見誤解

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

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

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

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





## 已採用的推導導讀

[實數：在 Cauchy 完備化中證明「循環的 9」與有理數 1 是同一個實數](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-real-number-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有理數](https://ocme.evemisslab.com/zh-Hant/mko/mko-rational-number/) — 本條目以有理數的嵌入與完備化建立實數入口。





## 驗證界線

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

not_formalized

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





## 下一個義務

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





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/real-number.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-number/index.md)