# 函數極限：可去因子商、仿射 δ 界與不等的單側極限

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-limit/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-function-limit-01 · production-20261019-adopted-96



## 目標與範圍

在去心實數論域上：(1) 以 ε-δ 證明 f(x)=(x²−9)/(x−3) 滿足 lim_(x→3) f(x)=6，而 f(3) 仍無定義；(2) 對仿射 g(x)=4x−1 在 a=2、ε=1/2，證明 δ=1/8 合法（等號 |m|δ=ε 允許），δ=1/7 不合法；(3) 對分支函數 h(x)=x+1（x<1）、h(x)=2x+3（x>1），求左右極限 2 與 5，並證明兩側極限不存在。

只處理 MKO 的三類題：仿射式、可去因子商、左右仿射分支，論域為 ℝ∖{a}。不證明一般極限定律（和、積、合成），不處理孤立點或其他接近論域。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- abs_rules
- order_basics
- frac_rules
- distributive
- func_limit_def
- numeric_evaluation


- G1 — 函數定義在去心論域 ℝ∖{a} 上；不要求 f(a) 存在。
- G2 — f(x)=(x²−9)/(x−3)，論域 ℝ∖{3}。
- G3 — g(x)=4x−1（m=4、b=−1），a=2；ε=1/2（p=1、q=2）；候選 δ=1/8（u=1、v=8）與 δ=1/7。
- G4 — h(x)=x+1（x<1），h(x)=2x+3（x>1），論域 ℝ∖{1}。


- \lim_{x\to a}f(x)=L — 去心兩側極限
- \varepsilon,\ \delta — 輸出容差與輸入距離界，皆為正
- 0<|x-a|<\delta — 去心鄰域：x≠a 且距離嚴格小於 δ
- \varepsilon=\tfrac{p}{q},\ \delta=\tfrac{u}{v} — 有理容差與有理距離界
- L^-,\ L^+ — 左極限與右極限





## 規則與來源


- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_func_limit · cited — 對在 a 附近所有 x≠a 都有定義的實函數 f，lim_(x→a) f(x)=L 指每個 ε>0 都有 δ>0，使 0<|x−a|<δ 時 |f(x)−L|<ε；左右有限極限必須相等才有兩側極限。仿射 mx+b 的極限為 ma+b；ε=p/q、δ=u/v 的仿射均勻界允許 |m|uq≤pv，等號合法。 · mko-function-limit
- one_sided_def · prerequisite — 左極限 L⁻：每個 ε>0 都有 δ>0，使 a−δ<x<a 時 |f(x)−L⁻|<ε；右極限 L⁺：a<x<a+δ 時 |f(x)−L⁺|<ε。
- L_affine_bound · lemma — 對 g(x)=mx+b、實數 a、ε>0、δ>0：若 |m|δ≤ε，則 0<|x−a|<δ 推出 |g(x)−(ma+b)|<ε。





## 逐步主鏈

S01 · definition操作前

\lim_{x\to a}f(x)=L

操作後

\forall\varepsilon>0\ \exists\delta>0\ \forall x:\ 0<|x-a|<\delta\Rightarrow|f(x)-L|<\varepsilon

條件：無

規則：mko_func_limit · 依賴：G1, func_limit_def

葉節點依據：func_limit_def + def_unfold

依 MKO 展開去心極限。條件 0<|x−a|<δ 排除 x=a，所以 f(a) 是否存在、取什麼值都不進入定義；輸入距離是嚴格小於 δ，輸出誤差也是嚴格小於 ε。



S02 · implies操作前

\mathrm{dom}(f)=\mathbb{R}\setminus\{3\}

操作後

\forall\delta>0:\ \{x:0<|x-3|<\delta\}\subseteq\mathrm{dom}(f),\ 3+\tfrac{\delta}{2}\ \text{in it}

條件：無

規則：mko_func_limit · 依賴：G2, S01

葉節點依據：set_builder + order_basics

去心鄰域中的 x 都滿足 x≠3，所以都在 f 的論域內；而且 3+δ/2 屬於它（0<δ/2<δ），鄰域不空。因此「x→3 時 f 的極限」是有意義的問題，雖然 f(3)=(9−9)/(3−3) 是 0/0，沒有定義。



S03 · equivalent操作前

x^2-9

操作後

(x-3)(x+3)

條件：無

規則：distributive · 依賴：G2, distributive

葉節點依據：distributive + add_inverse + add_zero

以分配律展開 (x−3)(x+3)=x²+3x−3x−9=x²−9，這是對所有實數 x 成立的恆等式（N1）。



S04 · equivalent操作前

f(x)=\frac{(x-3)(x+3)}{x-3}\ (x\neq 3)

操作後

f(x)=x+3\ (x\neq 3)

條件：x-3\neq 0

規則：frac_rules · 依賴：S03, frac_rules

葉節點依據：frac_rules + mul_inverse_nonzero

對 x≠3，x−3≠0，可以約去公因子：(x+3)(x−3)/(1·(x−3))=(x+3)/1（a/b=(ak)/(bk)，k=x−3≠0）。這只在論域 ℝ∖{3} 上成立；它不給 f 在 3 的值，因為在 3 約分要除以 0。



S05 · equivalent操作前

|f(x)-6|\ (x\neq 3)

操作後

|(x+3)-6|=|x-3|

條件：x\neq 3

規則：eq_replace · 依賴：S04

葉節點依據：eq_replace + add_assoc + add_inverse

在 x≠3 處以 S04 代入 f(x)=x+3，(x+3)−6=x−3。輸出誤差恰等於輸入距離。



S06 · implies操作前

\varepsilon>0\ \text{arbitrary},\ \delta=\varepsilon

操作後

0<|x-3|<\delta\Rightarrow|f(x)-6|=|x-3|<\varepsilon;\ \lim_{x\to 3}f(x)=6

條件：\varepsilon>0

規則：forall_intro · 依賴：S01, S02, S05

葉節點依據：forall_intro + exists_intro + func_limit_def

取任意 ε>0，令 δ=ε>0。若 0<|x−3|<δ，則 x≠3，由 S05，|f(x)−6|=|x−3|<δ=ε。ε 任意，依全稱推廣及 S01，lim_(x→3) f(x)=6。極限 6 不是 f(3)：f(3) 依然無定義（S02）。



S07 · equivalent操作前

|g(x)-7|,\ g(x)=4x-1,\ 7=4\cdot 2-1

操作後

|4x-8|=|4(x-2)|=4|x-2|

條件：無

規則：abs_rules · 依賴：G3, abs_rules

葉節點依據：abs_rules + distributive + numeric_evaluation

仿射極限值 ma+b=4·2−1=7（MKO 假設 a2）。g(x)−7=4x−8=4(x−2)（N3），依 |uv|=|u||v|，|g(x)−7|=4|x−2|。



S08 · equivalent操作前

|m|\cdot\frac{u}{v}\le\frac{p}{q}

操作後

|m|\,u\,q\le p\,v

條件：q>0; v>0

規則：order_basics · 依賴：G3, frac_rules

葉節點依據：order_basics + frac_rules

兩邊同乘正數 qv，不等號方向不變，得整數判準 |m|uq≤pv，即 MKO 假設 a3 的形式。這裡是「≤」，等號允許。



S09 · theorem_application操作前

4\cdot 1\cdot 2=8\le 8=1\cdot 8

操作後

0<|x-2|<\tfrac18\Rightarrow|g(x)-7|<\tfrac12

條件：|m|\delta\le\varepsilon

規則：L_affine_bound · 依賴：S07, S08, G3

葉節點依據：abs_rules + order_basics + case_analysis

代入 m=4、u=1、v=8、p=1、q=2：|m|uq=8≤8=pv，等號成立，即 |m|δ=4·(1/8)=1/2=ε。依引理 L_affine_bound，δ=1/8 合法。等號可以，因為輸入距離嚴格小於 δ：4|x−2|<4·(1/8)=1/2。引理在 S09.1 至 S09.3 證明。



S10 · implies操作前

\delta=\tfrac17:\ 4\cdot 1\cdot 2=8>7=1\cdot 7

操作後

x=2+\tfrac18:\ 0<|x-2|<\tfrac17,\ |g(x)-7|=\tfrac12\not<\tfrac12

條件：無

規則：quantifier_negation · 依賴：S07, S08, G3

葉節點依據：quantifier_negation + numeric_evaluation + order_basics

δ=1/7 時判準 8≤7 不成立。這時引理不適用，但還要證明 δ=1/7 真的不合法：取 x=2+1/8，|x−2|=1/8<1/7 且 x≠2，而 |g(x)−7|=4·(1/8)=1/2，不小於 ε=1/2。一個反例就否定了「所有 0<|x−2|<1/7 的 x 都合格」。



S11 · implies操作前

x<1:\ |h(x)-2|

操作後

|(x+1)-2|=|x-1|;\ \delta=\varepsilon\ \text{gives}\ L^-=2

條件：x<1

規則：one_sided_def · 依賴：G4, one_sided_def

葉節點依據：one_sided_def + abs_rules + forall_intro

左側 x<1 時 h(x)=x+1，(x+1)−2=x−1（N9）。對任意 ε>0 取 δ=ε：若 1−δ<x<1，則 |h(x)−2|=|x−1|<δ=ε。所以左極限是 2，即左分支 1·1+1 的值。



S12 · implies操作前

x>1:\ |h(x)-5|

操作後

|(2x+3)-5|=2|x-1|;\ \delta=\tfrac{\varepsilon}{2}\ \text{gives}\ L^+=5

條件：x>1

規則：one_sided_def · 依賴：G4, one_sided_def

葉節點依據：one_sided_def + abs_rules + forall_intro

右側 x>1 時 h(x)=2x+3，(2x+3)−5=2(x−1)（N10）。取 δ=ε/2：若 1<x<1+δ，則 |h(x)−5|=2|x−1|<2δ=ε。所以右極限是 5，即右分支 2·1+3 的值。



S13 · implies操作前

\lim_{x\to 1}h(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac32

操作後

\delta>0,\ t=\tfrac{\delta}{2}:\ |h(1+t)-L|<\tfrac32,\ |h(1-t)-L|<\tfrac32

條件：無

規則：exists_elim · 依賴：S01, G4

葉節點依據：exists_elim + forall_elim + order_basics

反證：假設兩側極限 L 存在。對 ε=3/2，定義給出某個 δ>0。令 t=δ/2，則 0<t<δ，點 1+t 與 1−t 都滿足 0<|x−1|<δ，所以 |h(1+t)−L|<3/2 且 |h(1−t)−L|<3/2。選 ε=3/2 是因為左右極限相差 3，3/2 是其一半。



S14 · implies操作前

|h(1+t)-h(1-t)|\le|h(1+t)-L|+|L-h(1-t)|<3

操作後

h(1+t)-h(1-t)=3+3t>3:\ \text{contradiction};\ \lim_{x\to 1}h(x)\ \text{does not exist}

條件：t>0

規則：contradiction · 依賴：S13, abs_rules

葉節點依據：contradiction + abs_rules + order_basics + numeric_evaluation

三角不等式與 |L−h(1−t)|=|h(1−t)−L| 給出 |h(1+t)−h(1−t)|<3/2+3/2=3。但直接計算 h(1+t)−h(1−t)=(2(1+t)+3)−((1−t)+1)=3+3t（N11），因 t>0，它大於 3，絕對值也大於 3。矛盾，所以兩側極限不存在。



S15 · implies操作前

\text{S06, S09, S10, S11, S12, S14}

操作後

\lim_{x\to3}f=6;\ \delta=\tfrac18\ \text{valid},\ \tfrac17\ \text{not};\ L^-=2\neq 5=L^+,\ \text{no two-sided limit}

條件：無

規則：and_intro_elim · 依賴：S06, S09, S10, S11, S12, S14

葉節點依據：and_intro_elim

匯總三個結論。對 h，兩個單側極限 2 與 5 都合法存在，只是不相等，所以只否定兩側極限；不能把其中一側抹掉，也不能以 h(1)（無定義）來補。







## 局部子步與引理

S09.1 · equivalent操作前

|(mx+b)-(ma+b)|

操作後

|m(x-a)|=|m|\,|x-a|

條件：無

規則：abs_rules · 依賴：distributive, abs_rules

葉節點依據：distributive + abs_rules + add_inverse

(mx+b)−(ma+b)=mx−ma=m(x−a)（N13），再用 |uv|=|u||v|。對任何 m、a、b、x 成立。



S09.2 · implies操作前

m=0

操作後

|g(x)-(ma+b)|=0<\varepsilon\ \text{for every}\ x

條件：m=0

規則：mul_zero · 依賴：S09.1, mul_zero

葉節點依據：mul_zero + order_basics

情況 m=0：由 S09.1，誤差為 0·|x−a|=0<ε，對任何 x 成立，所以任何正 δ 都合法（MKO 假設 a3）。



S09.3 · implies操作前

m\neq 0,\ 0<|x-a|<\delta,\ |m|\delta\le\varepsilon

操作後

|m||x-a|<|m|\delta\le\varepsilon

條件：|m|>0

規則：order_basics · 依賴：S09.1, order_basics

葉節點依據：order_basics + case_analysis

情況 m≠0：|m|>0，把嚴格不等式 |x−a|<δ 兩邊乘正數 |m|，得 |m||x−a|<|m|δ；再接上 |m|δ≤ε，依序的傳遞得嚴格的 |g(x)−(ma+b)|<ε。嚴格性來自輸入的 <δ，所以 |m|δ=ε 的等號情形也合法。兩個情況涵蓋所有 m，S09.1 至 S09.3 證得引理 L_affine_bound。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S06, S09, S10, S11, S12, S14 — 目標 G：本稿的三個結論。每一部分已由所列步驟正向證成；本步只合取，未把 G 當作前提。
- S14 · premise_audit · S13, abs_rules, contradiction — 矛盾只否定了「兩側極限存在」這個假設；S11、S12 的單側極限不受影響。
- S13 · premise_audit · S01, exists_elim, forall_elim — δ 是由假設取出的新名字；之後的結論不含 δ。
- S12 · premise_audit · G4, one_sided_def, forall_intro — 只用右分支在 x>1 的公式；兩個單側極限各自存在。
- S11 · premise_audit · G4, one_sided_def, forall_intro — 只用左分支在 x<1 的公式；ε 任意。
- S10 · premise_audit · S07, quantifier_negation, numeric_evaluation — 判準失敗本身只說明引理不適用；不合法的結論來自具體反例（N6、N7、N8）。
- S09.3 · premise_audit · S09.1, order_basics — 需要 |m|>0 才能保持嚴格不等號；m=0 已在 S09.2 另行處理。
- S09.2 · premise_audit · S09.1, mul_zero — 只需 ε>0；這是引理的第一個情況。
- S09.1 · inverse_equivalence · distributive, abs_rules — 恆等式，雙向成立。
- S09 · premise_audit · S08, L_affine_bound, numeric_evaluation — 引理的前提 |m|δ≤ε 以 N4、N5 核對；引理只給出充分條件。
- S08 · inverse_equivalence · order_basics, frac_rules — 反向是同除以正數 qv。
- S07 · inverse_equivalence · abs_rules, distributive — 恆等變形，雙向成立。
- S06 · sufficient_goal_reduction · S01, S05, forall_intro — 目標 G：極限為 6。足夠條件 H：對任意 ε，δ=ε 有效；H⇒G 由定義。H 由 S05 正向證成，未把 G 當作前提，也沒有用到 f(3)。
- S05 · inverse_equivalence · S04, eq_replace — 等值代換，雙向成立；只在 x≠3 使用。
- S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero — 反向是分子分母同乘 x−3，需要 x−3≠0；條件在論域內處處成立。
- S03 · inverse_equivalence · distributive — 恆等式，雙向成立。
- S02 · premise_audit · G2, S01, order_basics — 只確認極限問題有意義（3 是論域的極限點）；不宣稱極限存在。
- S01 · premise_audit · G1, mko_func_limit, func_limit_def — 此步只展開定義，不推出新事實。





## 錯誤控制與反例

分清極限與 f(a)，不能除零後補值MKO 的誤解之一是把極限當 f(a)。f(3) 是 0/0，沒有定義；極限 6 來自 x≠3 處的化簡 f(x)=x+3（S04），而 0<|x−3| 把中心排除在外（S01）。化簡不等於在 3 定義了 f；若另外定義 f(3)=100，極限仍是 6。

δ 邊界的等號合法另一個誤解是把 |m|δ=ε 當成不合法。因為輸入距離嚴格小於 δ，4|x−2|<4δ=ε 仍是嚴格的（S09.3），所以 δ=1/8 合法。這和數列尾界不同：那裡比較的是誤差本身，誤差等於 ε 不合格。δ=1/7 不合法則要用具體反例證明（S10）。

單側極限不等只否定兩側極限h 的左右極限 2 與 5 都存在，只是不等，所以兩側極限不存在（S14）。這不表示右極限不存在，也不能用有限個測點（例如 x=0.9、1.1）代替 ε-δ 論證。


- f(3)=0/0 沒有定義，所以 lim_(x→3) f(x) 不存在 → reject — 去心極限不看 f(3)；S06 證得極限為 6。
- f(x)=x+3，所以 f(3)=6 → reject — 化簡只在 x≠3 成立；f 的論域是 ℝ∖{3}，在 3 約分要除以 0。
- ε=1/2 時 δ=1/8 不合法，因為 |m|δ 恰等於 ε → reject — 0<|x−2|<1/8 給出 4|x−2|<1/2，嚴格不等成立。
- h 在 1 的兩側極限不存在，所以右極限也不存在 → reject — 右極限為 5（S12）；只是不等於左極限 2。
- f(3.1)=6.1、f(2.9)=5.9，所以極限為 6 已得證 → reject — 有限測點只與結論相容，不是證明；證明是 S06 對任意 ε 的論證。





## 結論與限制

f(x)=(x²−9)/(x−3) 在 ℝ∖{3} 上滿足 lim_(x→3) f(x)=6（δ=ε），而 f(3) 仍無定義。g(x)=4x−1 在 a=2、ε=1/2：δ=1/8 合法（4·1·2=8≤8，等號允許），δ=1/7 不合法（x=2+1/8 的誤差恰為 1/2）。h 的左極限為 2、右極限為 5，兩側極限不存在。


- 本稿不證明一般極限定律，也不處理論域含孤立點的情形。
- N2 是兩個測點的數值核對，只與 S04 的化簡相容，不參與證明。





## 驗證及來源綁定

14 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
- original source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-function-limit-01.json)