單射與不同輸入的辨識

數學敘述

給定總函數 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′) 字典序選首對，不從示意箭頭或抽樣猜性質。

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

已採用的推導導讀

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

前置知識

• 函數映射 — 先驗總函數輸入／輸出資格。
• 量詞與明示論域 — 單射條件量化兩個合法輸入。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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