# 實函數的點值與連續

在全實數論域連續需要點值存在且與兩側極限一致；補點與原函數連續不可混用。

mko-continuity · definition · v0.10.0



## 數學敘述

對f:R→R，f在a連續指每個ε>0都有δ>0，使 |x−a|<δ時 |f(x)−f(a)|<ε。等價地去心兩側極限等於已定義點值f(a)。本輪兩側仿射、中心明示值V的模型，在a連續當且僅當左極限=右極限=V。





## 代表公式（精確 TeX）

C(f,a)





## 成立條件


- 全實數論域及中心點值已明示，不把未定義中心直接稱作此論域上的不連續點。
- 仿射點值題精確算ma+b；分支題分別算left_m*a+left_b及right_m*a+right_b，中心值V獨立給定。
- 補定可去商的中心值以形成全R連續延拓時，唯一所需值為2a；補點前原商仍只在R∖{a}有定義。





## 符號作用域


- C — 全實數函數在一點連續的述詞
- f — 指定全實數總函數或補點後目標
- a — 明示實數中心





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

左右極限相等仍不足以連續，還須等於中心值；中心值只等於其中一側但另一側不同也不連續。

補點題問的是如何定義新的全實數延拓，不把原本去心商已經當成有中心值的總函數。可去不等於不需補定。

點缺陷對 (左極限−V,右極限−V) 精確顯示失配；二者都零才符合本模型的中心連續。共同平移全部輸出不產生新缺陷計算，改旁側斜率卻保持兩側極限也不充量。

左右極限相等就忽略點值，或未補定便聲稱原商在中心連續。





## 已採用的推導導讀

[連續：分支函數的中心值與可去商的唯一補點](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-continuity-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [去心實數論域的函數極限](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-limit/) — 先核對兩側極限。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 點值是總函數宣告的一部分。





## 驗證界線

明示分支與補點條件可重算；一般連續性理論與形式 Evidence 尚未建立。

not_formalized

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





## 下一個義務

在固定版綁定 ContinuousAt、full real domain與補點延拓，不混用去心極限及未定義點。





## 同源結構化資料

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

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