趨近關係：x→a 不是 x=a，也不保證函數值收斂

目標與範圍

在 (ℝ, 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|<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。
• 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 — 對實數 0<u≤v：1/v≤1/u。
• L_half · lemma — 對實數 δ>0：0<δ/2<δ。
• L_abs_neg · lemma — 對實數 u：|−u|=|u|。

逐步主鏈

\text{a structure for nearness}

(\mathbb{R},d),\ d(x,y)=|x-y|,\ a=1

n\ \text{a positive integer}

x_n=1+\tfrac1n>1,\ x_n\neq 1

x_n\to 1

\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ |x_n-1|<\varepsilon

|x_n-1|

\tfrac1n

\varepsilon>0\ \text{arbitrary}

N\in\mathbb{N},\ N>\tfrac1\varepsilon,\ N\ge 1

n\ge N\ge 1

\tfrac1n\le\tfrac1N

N>\tfrac1\varepsilon

\tfrac1N<\varepsilon

|x_n-1|=\tfrac1n\le\tfrac1N<\varepsilon\ \ (n\ge N)

x_n\to 1,\ \text{while}\ x_n\neq 1\ \text{for every}\ n

x_n>1\ \text{for every}\ n

g(x_n)=1\ \text{for every}\ n,\ g(x_n)\to 1

\lim_{x\to 1}g(x)=L

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

\lim_{x\to 1}g(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac12

\delta>0:\ 0<|x-1|<\delta\Rightarrow|g(x)-L|<\tfrac12

p=1+\tfrac\delta2,\ q=1-\tfrac\delta2

0<|p-1|<\delta,\ 0<|q-1|<\delta,\ g(p)=1,\ g(q)=0

\text{S11 applied at}\ x=p\ \text{and}\ x=q

|1-L|<\tfrac12,\ |0-L|<\tfrac12

|1-L|<\tfrac12,\ |0-L|<\tfrac12

1<1\ (\text{contradiction});\ \lim_{x\to 1}g(x)\ \text{does not exist}

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}

局部子步與引理

0<u\le v

\tfrac1v\le\tfrac1u

\delta>0

0<\tfrac\delta2<\delta

|-u|

|u|

1=|1-0|=|(1-L)+(L-0)|

1\le|1-L|+|0-L|<\tfrac12+\tfrac12=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=1

MKO 指出常見誤解是把 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、反控制與修訂記錄）