# 單射與不同輸入的辨識

單射要求不同合法輸入不能有同一輸出，不要求覆蓋整個陪域。

mko-injective · definition · v0.10.0



## 數學敘述

給定總函數 f:A→B，若對任意 x、y∈A，f(x)=f(y) 蘊涵 x=y，則 f 為單射；等價地，不同輸入具有不同輸出。每個 b∈B 的原像纖維 {x∈A:f(x)=b} 至多有一個元素。





## 代表公式（精確 TeX）

f:A\to B





## 成立條件


- A、B 與總函數已明示；每個 A 中輸入恰有一個 B 中輸出。
- 題庫是有限整數標籤的函數表；空定義域的單射條件真，不外推有限結果到其他函數。





## 符號作用域


- f — 指定總函數
- A — 定義域
- B — 陪域





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

先檢查表格在 A 上總定義，再比較不同輸入的輸出。重複列出同一有序對只是表示重複；同一輸入配不同輸出則不是總函數。

單射可以漏掉陪域的元素。纖維大小可以是零或一；只有同一輸出有兩個不同原像時，才得到單射失敗的碰撞見證。

限制到 C⊆A 後，所得函數只比較 C 中輸入；原函數可能不單射而限制後單射。有限首碰撞先取 x<x′，再按 (x,x′) 字典序選首對，不從示意箭頭或抽樣猜性質。

把單射誤當每個陪域元素都有原像，或略過總函數資格。





## 已採用的推導導讀

[單射與不同輸入的辨識：函數表的資格、碰撞見證與纖維](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-injective-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 先驗總函數輸入／輸出資格。
- [量詞與明示論域](https://ocme.evemisslab.com/zh-Hant/mko/mko-quantifier/) — 單射條件量化兩個合法輸入。





## 驗證界線

有限表可完整檢查單射及碰撞；一般單射理論未新增形式 Evidence。

not_formalized

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





## 下一個義務

綁定 Function.Injective、纖維基數與定義域限制。





## 同源結構化資料

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

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