# 去心實數論域的函數極限

在a附近排除a本身，以ε-δ控制函數值；點值不屬於去心極限條件。

mko-function-limit · definition · v0.10.0



## 數學敘述

對在a附近所有x≠a都有定義的實函數f，lim_(x→a)f(x)=L，指每個ε>0都有δ>0，使0<|x−a|<δ時 |f(x)−L|<ε。本輪用仿射式、可去因子商及左右仿射分支，左右有限極限必須相等才有兩側極限。





## 代表公式（精確 TeX）

L(f,a)





## 成立條件


- 題庫函數採去心實數論域R∖{a}，不要求f(a)存在，不包含孤立點或其他未明示的接近論域。
- 仿射mx+b的極限為ma+b；(x²−a²)/(x−a)只在x≠a可消因子，極限為2a，不因此給原商在a的值。
- 正有理ε=p/q、δ=u/v的仿射均勻界允許 |m|u q≤p v；等號合法，因輸入距離嚴格小於δ。m=0時所有正δ合法。





## 符號作用域


- L — 去心實數極限運算
- f — 在中心外有定義的指定函數
- a — 實數接近中心





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

去心極限排除中心，因此原函數在中心未定義或改了中心值，都不直接改變這個極限。這和連續性需要中心點值不同。

仿射界從 |f(x)−(ma+b)|=|m||x−a| 得到。輸入距離嚴格小於δ，故 |m|δ=ε仍可保證輸出嚴格小於ε；不要將數列尾界的嚴格比較原樣套過來。

左右仿射分支各自有極限；兩側值不相等時兩側有限極限不存在。只否定此兩側極限，不把其中一側的合法極限抹掉，也不以有限測點替一般函數背書。

把極限當f(a)、除零後補值，或把δ邊界等號誤判為不合法。





## 已採用的推導導讀

[函數極限：可去因子商、仿射 δ 界與不等的單側極限](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-function-limit-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 函數的定義域與陪域。
- [趨近關係](https://ocme.evemisslab.com/zh-Hant/mko/mko-tends-to-relation/) — 接近點不等於直接代入。
- [絕對值](https://ocme.evemisslab.com/zh-Hant/mko/mko-absolute-value/) — 實數距離與ε-δ誤差。
- [有理係數多項式因式分解](https://ocme.evemisslab.com/zh-Hant/mko/mko-factorization/) — 在非零分母前提下消去x−a。





## 驗證界線

明示仿射／可去商／兩側模型可精確核對；一般函數極限與型別橋未附形式 Evidence。

not_formalized

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





## 下一個義務

綁定 punctured nhds、左右鄰域與仿射誤差界；不以總定義除零API替代去心資格。





## 同源結構化資料

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

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