實函數的點值與連續

數學敘述

對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) 精確顯示失配；二者都零才符合本模型的中心連續。共同平移全部輸出不產生新缺陷計算，改旁側斜率卻保持兩側極限也不充量。

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

已採用的推導導讀

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

前置知識

• 去心實數論域的函數極限 — 先核對兩側極限。
• 函數映射 — 點值是總函數宣告的一部分。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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