# 雙射的反函數

雙射 f:A→B 的反函數 g:B→A 須驗證兩個方向的還原，不能把交換資料當成無條件反函數。

mko-inverse-function · definition · v0.10.0



## 數學敘述

若 f:A→B 是雙射，反函數 g:B→A 由每個 b 的唯一原像定義，滿足 g(f(x))=x（x∈A）及 f(g(y))=y（y∈B）。有限表可以交換有序對後建立 g；若 f 非雙射，交換表不能自動成為這個 B→A 的反函數。





## 代表公式（精確 TeX）

g(f(x))=x





## 成立條件


- 反函數表與求值題先確認 f 是宣告 A→B 的雙射。
- 候選 g 先驗為總函數 B→A，再查兩側 identity；代表公式只呈現其中一側。
- 仿射例子限定 f:R→R、m≠0；inverse 的係數以最簡正分母有理數回答。





## 符號作用域


- g — 反函數或候選總函數
- f — 宣告雙射
- x — A 中合法輸入





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

在有限雙射表中，每個目標恰出現一次，交換後才是總函數 B→A。空雙射 ∅→∅ 的 inverse 也是空函數。

反函數按兩側 identity 定義；本輪候選驗收逐側檢查，避免把一般單側 inverse 當成雙側 inverse。候選表需完整明示陪域／定義域。反函數不是取倒數 1/f(x)。

對 f(x)=mx+b 且 m≠0，g(y)=(y−b)/m；寫成 g(y)=uy+v 時 u=1/m、v=−b/m。本輪只算精確整數參數的有理係數，不聲稱一般可逆映射的機器證明已完成。

非雙射也交換表就叫反函數，或把 f⁻¹ 當成 1/f。





## 已採用的推導導讀

[反函數：交換有限雙射表並求非零斜率仿射函數的反函數](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-inverse-function-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [雙射與唯一原像](https://ocme.evemisslab.com/zh-Hant/mko/mko-bijective/) — 反函數需要每個目標的唯一原像。
- [函數合成](https://ocme.evemisslab.com/zh-Hant/mko/mko-composition/) — 兩個方向的還原以合成描述。
- [仿射函數與一次函數](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-function/) — 非零斜率的實仿射函數例子。





## 驗證界線

明示有限雙射可驗證兩側還原；一般 inverse 存在唯一性與型別橋仍待形式化。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定 Function.LeftInverse／RightInverse、Equiv.symm 和非零仿射 inverse。





## 同源結構化資料

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

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