趨近關係

數學敘述

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 或 ε–δ 定義。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 函數映射 — 函數極限會在輸入趨近時研究映射值的行為。

驗證界線

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

formalized_filter_tendsto_core

• evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d

下一個義務

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

同源結構化資料

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