# 趨近關係：x→a 不是 x=a，也不保證函數值收斂 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-tends-to-relation/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-tends-to-relation-01 · production-20261019-adopted-96 ## 目標與範圍在 (ℝ, d(x,y)=|x−y|) 中：(1) 證明數列 x_n=1+1/n 趨近 1，而每一項都有 x_n≠1；(2) 對 g(x)=1（x>1）、g(x)=0（x≤1），證明沿 x_n 有 g(x_n)→1，但 lim_{x→1} g(x) 不存在。由此說明 x→1 本身既不要求 x 等於 1，也不決定函數值是否收斂。在 MKO 假設 a1 之下工作：明示的度量結構 (ℝ,|x−y|)。使用標準的數列極限與 ε–δ 函數極限定義作為前置知識。不建立 Mathlib 的 Filter.Tendsto、nhds 或 atTop 物件，也不證明它們與 ε–δ 定義的等價；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - metric_def - abs_rules - order_basics - archimedean - seq_limit_def - func_limit_def - G1 — 結構：實數集 ℝ 配上度量 d(x,y)=|x−y|（假設 a1）；目標點 a=1。 - G2 — 數列 x_n=1+1/n，n 取遍所有正整數。 - G3 — 函數 g:ℝ→ℝ：x>1 時 g(x)=1，x≤1 時 g(x)=0。 - x\to a — 趨近關係（方向性語言） - x_n — 數列 1+1/n - g — 在 1 處跳躍的函數 - \varepsilon,\ \delta — 目標端與來源端的容許距離 - N — 依賴 ε 的索引門檻 - d(x,y)=|x-y| — ℝ 上的標準度量 ## 規則與來源 - metric_def · prerequisite — 度量：d:X×X→ℝ 滿足 d(x,y)≥0 且 d(x,y)=0 ⇔ x=y；d(x,y)=d(y,x)；三角不等式 d(x,z)≤d(x,y)+d(y,z)。 - abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|v 之一；u0 推出 uwvw。 - archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。 - seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。 - func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - add_zero · prerequisite — 加法單位元：u+0=u。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - 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）。 - logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。 - modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_tends_to · cited — x→a 是極限語言中的方向性關係；它本身尚未指定函數值是否收斂，也不等同於 x 最終必須等於 a。 · mko-tends-to-relation - L_recip_le · lemma — 對實數 00：0<δ/2<δ。 - L_abs_neg · lemma — 對實數 u：|−u|=|u|。 ## 逐步主鏈 S01 · definition操作前 \text{a structure for nearness} 操作後 (\mathbb{R},d),\ d(x,y)=|x-y|,\ a=1 條件：無規則：metric_def · 依賴：G1 葉節點依據：metric_def + abs_rules 依 MKO 假設 a1，談趨近之前必須先指定能討論鄰近的結構。這裡取 ℝ 與度量 d(x,y)=|x−y|：它非負、只在 x=y 時為 0、對稱且滿足三角不等式（abs_rules）。目標點 a=1。之後「接近 1」都是指 |x−1| 小。 S02 · implies操作前 n\ \text{a positive integer} 操作後 x_n=1+\tfrac1n>1,\ x_n\neq 1 條件：n>0 規則：order_basics · 依賴：G2 葉節點依據：order_basics + mul_inverse_nonzero + add_zero + forall_intro 對每個正整數 n，1/n>0（正數的倒數為正：若 1/n≤0，乘以 n>0 會得 1≤0，矛盾）。依序的加法性質，x_n=1+1/n>1+0=1，所以 x_n≠1。數列沒有任何一項等於 1。 S03 · equivalent操作前 x_n\to 1 操作後 \forall\varepsilon>0\ \exists N\ \forall n\ge N:\ |x_n-1|<\varepsilon 條件：無規則：seq_limit_def · 依賴：S01, G2 葉節點依據：seq_limit_def + def_unfold 依數列極限定義展開 x_n→1。注意量詞次序：先任意給定 ε，再找 N（N 可以依賴 ε），然後對所有 n≥N 要求距離小於 ε。定義中沒有任何一處要求 x_n=1。 S04 · equivalent操作前 |x_n-1| 操作後 \tfrac1n 條件：\tfrac1n>0 規則：abs_rules · 依賴：G2, S02 葉節點依據：add_assoc + add_comm + add_inverse + add_zero + abs_rules x_n−1=(1+1/n)−1=1/n（加法結合律與反元素）。因 1/n>0（S02），依絕對值規則 |1/n|=1/n。所以 x_n 與 1 的距離恰好是 1/n。 S05 · implies操作前 \varepsilon>0\ \text{arbitrary} 操作後 N\in\mathbb{N},\ N>\tfrac1\varepsilon,\ N\ge 1 條件：\varepsilon>0 規則：archimedean · 依賴：S03 葉節點依據：archimedean + exists_elim + mul_inverse_nonzero 任意取 ε>0，則 1/ε 是正實數。依阿基米德性質，存在自然數 N>1/ε；因 1/ε>0，N>0，所以 N≥1。N 依賴 ε：ε 越小，需要的 N 越大。例如 ε=1/10 時 1/ε=10，可取 N=11。 S06 · implies操作前 n\ge N\ge 1 操作後 \tfrac1n\le\tfrac1N 條件：N>0 規則：L_recip_le · 依賴：S05 葉節點依據：order_basics + case_analysis + mul_inverse_nonzero 依引理 L_recip_le（在 S06.1 證明），取 u=N、v=n：由 0\tfrac1\varepsilon 操作後 \tfrac1N<\varepsilon 條件：\varepsilon>0; N>0 規則：order_basics · 依賴：S05 葉節點依據：order_basics + frac_rules + mul_inverse_nonzero ε/N>0（兩個正數之商）。兩邊同乘正數 ε/N：左邊 N·(ε/N)=ε，右邊 (1/ε)·(ε/N)=1/N，所以 ε>1/N，即 1/N<ε。 S08 · implies操作前 |x_n-1|=\tfrac1n\le\tfrac1N<\varepsilon\ \ (n\ge N) 操作後 x_n\to 1,\ \text{while}\ x_n\neq 1\ \text{for every}\ n 條件：無規則：forall_intro · 依賴：S02, S03, S04, S06, S07 葉節點依據：order_basics + forall_intro + logic_chain 對每個 n≥N：|x_n−1|=1/n（S04）≤1/N（S06）<ε（S07），依序的傳遞，|x_n−1|<ε。ε 是任意的正數，N 由 S05 給出，依 ∀引入，S03 的右邊成立，所以 x_n→1。結合 S02：x_n 趨近 1，但沒有任何一項等於 1。 S09 · implies操作前 x_n>1\ \text{for every}\ n 操作後 g(x_n)=1\ \text{for every}\ n,\ g(x_n)\to 1 條件：無規則：seq_limit_def · 依賴：S02, G3 葉節點依據：seq_limit_def + abs_rules + forall_intro 由 S02，每個 x_n>1，依 G3，g(x_n)=1。對任意 ε>0 取 N=1，所有 n 都有 |g(x_n)−1|=|0|=0<ε，所以 g(x_n)→1。沿著這一條趨近 1 的數列，函數值收斂到 1。 S10 · equivalent操作前 \lim_{x\to 1}g(x)=L 操作後 \forall\varepsilon>0\ \exists\delta>0\ \forall x:\ 0<|x-1|<\delta\Rightarrow|g(x)-L|<\varepsilon 條件：無規則：func_limit_def · 依賴：G3, S01 葉節點依據：func_limit_def + def_unfold 函數極限需要比裸箭頭 x→1 多得多的資料：目標值 L、量詞次序（先 ε 後 δ），以及去心鄰域條件 0<|x−1|<δ（x=1 本身被排除，所以 g(1) 的值不影響極限）。1 是定義域 ℝ 的極限點，定義適用。 S11 · implies操作前 \lim_{x\to 1}g(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac12 操作後 \delta>0:\ 0<|x-1|<\delta\Rightarrow|g(x)-L|<\tfrac12 條件：無規則：exists_elim · 依賴：S10 葉節點依據：forall_elim + exists_elim 為了反證，暫時假設某個實數 L 使 lim_{x→1} g(x)=L。把 S10 的定義用於 ε=1/2（∀消去），得到某個 δ>0（∃消去，取新名字 δ），使所有滿足 0<|x−1|<δ 的 x 都有 |g(x)−L|<1/2。 S12 · implies操作前 p=1+\tfrac\delta2,\ q=1-\tfrac\delta2 操作後 0<|p-1|<\delta,\ 0<|q-1|<\delta,\ g(p)=1,\ g(q)=0 條件：\delta>0 規則：L_half · 依賴：S11, G3 葉節點依據：order_basics + abs_rules + frac_rules 取 p=1+δ/2、q=1−δ/2。|p−1|=δ/2，|q−1|=|−δ/2|=δ/2。依引理 L_half（在 S12.1 證明），0<δ/2<δ，所以 p、q 都在去心鄰域內。又 p>1、q<1，依 G3，g(p)=1、g(q)=0。例如 δ=1/4 時 p=9/8、q=7/8，兩者與 1 的距離都是 1/8<1/4。 S13 · implies操作前 \text{S11 applied at}\ x=p\ \text{and}\ x=q 操作後 |1-L|<\tfrac12,\ |0-L|<\tfrac12 條件：無規則：forall_elim · 依賴：S11, S12 葉節點依據：forall_elim + modus_ponens + eq_replace p、q 都滿足 0<|x−1|<δ（S12），把 S11 的全稱語句分別代入 x=p 與 x=q：|g(p)−L|<1/2 與 |g(q)−L|<1/2；再代入 g(p)=1、g(q)=0。 S14 · implies操作前 |1-L|<\tfrac12,\ |0-L|<\tfrac12 操作後 1<1\ (\text{contradiction});\ \lim_{x\to 1}g(x)\ \text{does not exist} 條件：無規則：contradiction · 依賴：S13, L_abs_neg 葉節點依據：contradiction + order_basics + abs_rules + quantifier_negation 由 S14.1、S14.2 的計算得 1<1，與序的三一律矛盾。所以 S11 的暫時假設不成立：沒有任何實數 L 使 lim_{x→1} g(x)=L，即這個極限不存在。L 是任意的，所以結論對所有候選值成立。 S15 · implies操作前 x_n\to 1,\ x_n\neq 1,\ g(x_n)\to 1,\ \lim_{x\to 1}g(x)\ \text{does not exist} 操作後 x\to 1\ \text{neither forces}\ x=1\ \text{nor decides whether}\ g(x)\ \text{converges} 條件：無規則：mko_tends_to · 依賴：S08, S09, S14 葉節點依據：mko_tends_to + and_intro_elim 彙整並對照 MKO：(1) x_n→1 而每項 x_n≠1（S02、S08），所以趨近不要求等於；(2) 同樣在 1 附近，沿 x_n 的函數值收斂（S09），但完整的 ε–δ 極限不存在（S14），所以裸箭頭 x→1 本身不決定函數值是否收斂；要說「收斂」，還必須指定目標值、量詞次序與去心鄰域條件（S10）。 ## 局部子步與引理 S06.1 · implies操作前 00; v>0 規則：order_basics · 依賴：order_basics 葉節點依據：order_basics + case_analysis + frac_rules + mul_inverse_nonzero 分兩種情況。若 u=v，則 1/v=1/u。若 u0，1/(uv)>0；兩邊同乘正數 1/(uv) 保持不等號，u·1/(uv)0 操作後 0<\tfrac\delta2<\delta 條件：\delta>0 規則：order_basics · 依賴：order_basics 葉節點依據：order_basics + frac_rules + two_nonzero δ>0 兩邊乘以正數 1/2，得 δ/2>0。又 δ−δ/2=δ/2>0，兩邊加 δ/2 得 δ>δ/2。證得引理 L_half。 S14.1 · equivalent操作前 |-u| 操作後 |u| 條件：無規則：abs_rules · 依賴：abs_rules 葉節點依據：abs_rules + neg_mul + mul_one |−u|=|(−1)u|=|−1|·|u|（|uv|=|u||v|）。因 −1<0，|−1|=−(−1)=1，所以 |−u|=1·|u|=|u|。證得引理 L_abs_neg；之後用於 |L−0|=|−(0−L)|=|0−L|。 S14.2 · implies操作前 1=|1-0|=|(1-L)+(L-0)| 操作後 1\le|1-L|+|0-L|<\tfrac12+\tfrac12=1 條件：無規則：abs_rules · 依賴：S13, S14.1 葉節點依據：abs_rules + add_inverse + order_basics + numeric_evaluation 1=|1−0|，且 1−0=(1−L)+(L−0)（插入 −L+L=0）。依三角不等式，|(1−L)+(L−0)|≤|1−L|+|L−0|；依 L_abs_neg，|L−0|=|0−L|。再用 S13 的兩個不等式：|1−L|+|0−L|<1/2+1/2=1。合起來 1<1。 ## 逐步反向審查 - S15 · sufficient_goal_reduction · S08, S09, S14, mko_tends_to, and_intro_elim — 目標 G 是題目兩部分結論的合取；每一部分都由所列步驟正向證成，此步只做合取並與 MKO 對照，沒有把 G 當作前提。 - S14.2 · premise_audit · abs_rules, S13, S14.1, order_basics — 三角不等式是單向的（≤），兩個嚴格不等式相加得到嚴格不等式；整條鏈只需單向。 - S14.1 · inverse_equivalence · abs_rules, neg_mul, mul_one — 每一步都是恆等式，兩邊是同一個數，雙向成立。 - S14 · premise_audit · S13, contradiction, order_basics — 矛盾只來自 S11 的假設，因此被否定的正是「極限存在」；論證沒有對 L 做任何限制。 - S13 · premise_audit · S11, S12, forall_elim, eq_replace — 代入前必須先確認 p、q 滿足 S11 的前提（S12）。 - S12.1 · premise_audit · order_basics, frac_rules — 只用到乘以正數與加上同一數保持不等號；δ≤0 時結論不成立。 - S12 · premise_audit · L_half, abs_rules, G3 — 需要 δ>0 才有 0<δ/2<δ；p、q 都不等於 1，所以去心條件成立。|−δ/2|=δ/2 用到 δ/2>0 與絕對值規則。 - S11 · premise_audit · S10, forall_elim, exists_elim — 這是反證的暫時假設，在 S14 推出矛盾後釋放；δ 是新名字，最後結論不提到它。 - S10 · inverse_equivalence · func_limit_def — 定義的展開雙向成立。 - S09 · premise_audit · S02, G3, seq_limit_def — 結論只關於這一條數列；不宣稱 g 在 1 的極限存在，S14 證明它不存在。 - S08 · sufficient_goal_reduction · S03, S04, S05, S06, S07, forall_intro — 目標 G：x_n→1。足夠條件 H：對任意 ε>0 有 N 使 n≥N 時 |x_n−1|<ε；H⇒G 由 S03。H 由 S04 到 S07 正向證成，ε 是任意的，沒有把 G 當作前提。 - S07 · premise_audit · order_basics, frac_rules — 需要 ε/N>0 以保持不等號方向；這一步只用到 S05 的 N>1/ε。 - S06.1 · premise_audit · order_basics, case_analysis, frac_rules — 乘以正數保持不等號方向需要 1/(uv)>0；若 u 或 v 可為負，結論可能失敗（例如 u=−1、v=1 時 1/v=1>−1=1/u）。 - S06 · premise_audit · L_recip_le, S05 — 引理需要 u>0；這由 S05 的 N≥1 提供。 - S05 · premise_audit · archimedean, exists_elim — 需要 ε>0 才有 1/ε；N 的存在不是由試算幾個 ε 得到，而是由阿基米德性質對每個 ε 保證。 - S04 · inverse_equivalence · add_inverse, abs_rules, S02 — 兩邊是同一個數；|u|=u 需要 u≥0，S02 已給出 1/n>0。 - S03 · inverse_equivalence · seq_limit_def — 定義的展開與收回雙向成立。 - S02 · premise_audit · order_basics, mul_inverse_nonzero — 需要 n>0；結論對每個 n 成立，因為 n 是任意正整數。只推出 x_n>1，不宣稱反向。 - S01 · premise_audit · G1, metric_def, abs_rules — 此步只指定結構，不推出新事實；換一個度量或拓撲，鄰近的意義也會不同。 ## 錯誤控制與反例 x→1 不是 x=1MKO 指出常見誤解是把 x→a 直接讀成 x=a。數列 x_n 趨近 1，但每一項 x_n>1（S02、S08）。函數極限的定義更明確排除 x=1（0<|x−1|，S10）：g(1)=0 這個代入值既不是沿 x_n 的極限值 1，也不構成極限，因為極限根本不存在（S14）。一條路徑不等於完整定義MKO 也提醒不要把裸箭頭當成完整的 Filter.Tendsto 或 ε–δ 定義。沿 x_n 檢查得到 g(x_n)→1（S09），只涵蓋從右側趨近的一條數列；ε–δ 定義要求去心鄰域中所有 x，包括左側的 q（S12），因而極限不存在。量詞次序最容易做錯的是把「對每個 ε 存在 N」改成「存在 N 對每個 ε」。後者對 x_n 不成立：給定任何 N，取 ε=1/N、n=N，則 |x_N−1|=1/N 並不小於 ε（N10 以 N=3 為例）。S05 的 N 依賴 ε，這正是定義所允許的。 - x_n→1，所以某一項 x_n 等於 1 → reject — 每一項都有 x_n=1+1/n>1（S02）。 - 沿 x_n 有 g(x_n)→1，所以 lim_{x→1} g(x)=1 → reject — 左側的點 q 有 g(q)=0；S11 到 S14 證明極限不存在。 - x→1 就是代入 x=1，所以 lim_{x→1} g(x)=g(1)=0 → reject — 定義排除 x=1（S10），而且極限不存在（S14）。 - 存在 N，使對所有 ε>0 與所有 n≥N 都有 |x_n−1|<ε → reject — 取 ε=1/N、n=N，|x_N−1|=1/N 不小於 ε。 - 寫出 x→1 就已經說明 g(x) 收斂 → reject — MKO 指出趨近關係本身不指定函數值是否收斂；本例 g 在 1 的極限不存在（S14）。 ## 結論與限制在 (ℝ,|x−y|) 中，x_n=1+1/n 趨近 1，而沒有任何一項等於 1；對在 1 處跳躍的 g，沿 x_n 有 g(x_n)→1，但 lim_{x→1} g(x) 不存在（任何候選 L 都會導出 1<1）。所以 x→1 本身既不要求 x=1，也不決定函數值是否收斂；完整的極限語句還需要目標值、量詞次序與去心鄰域條件。 - 本稿只使用度量 |x−y| 下的 ε–N 與 ε–δ 定義；與 Mathlib 的 Filter.Tendsto、nhds、atTop 之對應未在本稿證明。 - N4 只在 n=1 到 50 核對 (1+1/n)−1=1/n，是有限檢查；一般情形由 S04 的加法規則證明。N1 到 N3、N5 到 N11 只是對具體數值的核對，論證不依賴它們。 ## 驗證及來源綁定 11 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 9cb369c6f946a7068f52b3a1c30a5922a592d1864238416d34c642fcdd014920 - original source SHA-256: 9cb369c6f946a7068f52b3a1c30a5922a592d1864238416d34c642fcdd014920 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-tends-to-relation-01.json)