# 趨近關係

符號 x→a 表示變數或索引所描述的狀態朝目標 a 趨近。

mko-tends-to-relation · concept · v0.8.0



## 數學敘述

x→a 是極限語言中的方向性關係；它本身尚未指定函數值是否收斂，也不等同於 x 最終必須等於 a。





## 代表公式（精確 TeX）

x\to a





## 成立條件


- 已指定可討論鄰近與趨近的數學結構，例如度量或拓撲。





## 符號作用域


- x — 變動表達式或變數
- a — 趨近目標
- → — 趨近關係





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

趨近描述的是一個過程或關係，不是單次代入。x 可以任意接近 a，而不必在討論中的每一步都等於 a。

完整函數極限還需要另外描述 f(x) 的目標值、量詞順序與鄰域條件；本物件只提供其中的趨近語義。

Mathlib 使用 Filter.Tendsto f l₁ l₂ 表達函數相對於來源與目標濾子的趨近，並在定義上等價於 Filter.map f l₁≤l₂。

把 x→a 直接解讀成 x=a，或在尚未指定來源與目標濾子時，宣稱裸箭頭已等同於完整 Filter.Tendsto 或 ε–δ 定義。





## 已採用的推導導讀

[趨近關係：x→a 不是 x=a，也不保證函數值收斂](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-tends-to-relation-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 函數極限會在輸入趨近時研究映射值的行為。





## 驗證界線

Lean 已形式化 Filter.Tendsto 的核心濾子語義；裸符號 x→a 仍必須補上函數與來源、目標濾子，且本證據不是特定函數極限。

formalized_filter_tendsto_core


- [evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d](https://ocme.evemisslab.com/data/evidence/38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d.json)





## 下一個義務

建立 atTop、nhds、nhdsWithin 等常用來源與目標濾子物件，再分別連接數列極限與函數點極限。





## 同源結構化資料

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

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