# 單射與不同輸入的辨識：函數表的資格、碰撞見證與纖維

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-injective/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-injective-01 · production-20261019-adopted-96



## 目標與範圍

設 A={1,2,3,4}、B={1,2,3,4,5,6}，函數表 f：(1,4),(2,6),(3,1),(4,5)；g：(1,4),(2,6),(2,6),(3,4),(4,6)；h：(1,4),(2,6),(2,5),(3,1),(4,5)。確認各表是否為總函數 A→B；判定 f、g 是否單射並列出纖維；找出 g 按字典序的首碰撞；判定 g 限制到 C={1,2} 是否單射；並說明空定義域的情形。

在 MKO 的範圍內工作：有限整數標籤的函數表。先檢查總函數資格，再以完整比較判定單射，並證明兩個一般小引理（只需比較 x<y 的輸入對；單射等價於每個纖維至多一個元素）。結果只針對這些表，不外推到其他函數；不處理無限定義域；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- image_preimage_def
- contrapositive
- quantifier_negation
- numeric_evaluation
- table_function


- G1 — A={1,2,3,4}，B={1,2,3,4,5,6}。
- G2 — 函數表（每列為 (輸入, 輸出)）：f：(1,4),(2,6),(3,1),(4,5)；g：(1,4),(2,6),(2,6),(3,4),(4,6)；h：(1,4),(2,6),(2,5),(3,1),(4,5)。
- G3 — C={1,2}⊆A；另考慮空定義域的函數 f₀:∅→B。


- f,\ g,\ h — 三張函數表
- f^{-1}(\{b\}) — b 的纖維 {x∈A ∣ f(x)=b}
- g|_C — g 限制到 C 的函數
- (x,x') — 碰撞對：x<x′ 且 g(x)=g(x′)
- \varnothing\to B — 空定義域的函數





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_injective_def · cited — 給定總函數 f:A→B，若對任意 x、y∈A，f(x)=f(y) 蘊涵 x=y，則 f 為單射；等價地，不同輸入具有不同輸出。每個 b∈B 的原像纖維 {x∈A:f(x)=b} 至多有一個元素。 · mko-injective
- table_function · prerequisite — 有限表格（列為 (x,y)）定義總函數 A→B，當且僅當：每列 x∈A、y∈B；每個 x∈A 至少出現在一列；同一 x 的各列輸出相同。完全相同的列只是同一個有序對的重複列出。
- roster_membership · prerequisite — 列舉集合的成員關係：對以列舉給出的有限集合 S={s_i ∣ 1≤i≤n}，z∈S 當且僅當存在 i 使 z=s_i。
- restriction_def · prerequisite — 對 C⊆A，f 限制到 C 的函數 f|_C:C→B 定義為 f|_C(x)=f(x)（x∈C）。
- lex_order · prerequisite — 整數對的字典序：(x,x′) 排在 (y,y′) 之前，當且僅當 x<y，或 x=y 且 x′<y′。
- empty_set_def · prerequisite — 空集合：對每個 x，x∉∅。
- L_pairs_lt · lemma — 對 A⊆ℤ 與函數 f:A→B：f 單射 ⇔ 對所有 x、y∈A 且 x<y，都有 f(x)≠f(y)。
- L_fiber · lemma — 對函數 f:A→B：f 單射 ⇔ 每個 b∈B 的纖維 f⁻¹({b}) 至多有一個元素。





## 逐步主鏈

S01 · implies操作前

f:\ (1,4),(2,6),(3,1),(4,5)

操作後

f:A\to B\ \text{total};\ f(1)=4,\ f(2)=6,\ f(3)=1,\ f(4)=5

條件：無

規則：table_function · 依賴：G1, G2, table_function

葉節點依據：table_function + roster_membership

MKO 第一段：先檢查表格在 A 上總定義。A 的四個輸入 1、2、3、4 各恰出現在一列，輸出 4、6、1、5 都在 B 中，沒有同一輸入配不同輸出。所以 f 是總函數 A→B。



S02 · equivalent操作前

\forall x,y\in A:\ f(x)=f(y)\Rightarrow x=y

操作後

\forall x,y\in A:\ x\neq y\Rightarrow f(x)\neq f(y)

條件：無

規則：contrapositive · 依賴：mko_injective_def, contrapositive

葉節點依據：mko_injective_def + contrapositive

依 MKO 的定義，單射是「f(x)=f(y) 蘊涵 x=y」。對每一對 x、y 取逆否命題，得「x≠y 蘊涵 f(x)≠f(y)」，即不同輸入有不同輸出。之後用這個形式逐對比較。



S03 · equivalent操作前

\forall x,y\in A:\ x\neq y\Rightarrow f(x)\neq f(y)

操作後

\forall x,y\in A:\ x<y\Rightarrow f(x)\neq f(y)

條件：A\subseteq\mathbb{Z}

規則：L_pairs_lt · 依賴：S02, L_pairs_lt

葉節點依據：case_analysis + order_basics

依引理 L_pairs_lt，只需比較 x<y 的輸入對；A 有 C(4,2)=6 個這樣的對（N2）。x=y 的情形不需比較，x>y 的情形與 y<x 重複。



S04 · implies操作前

(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)

操作後

4\neq 6,\ 4\neq 1,\ 4\neq 5,\ 6\neq 1,\ 6\neq 5,\ 1\neq 5;\ f\ \text{injective}

條件：無

規則：forall_intro · 依賴：S01, S03, forall_intro

葉節點依據：case_analysis + roster_membership + numeric_evaluation + forall_intro

逐一比較六個輸入對的輸出：f(1)=4 與 f(2)=6、f(3)=1、f(4)=5 都不同；f(2)=6 與 f(3)=1、f(4)=5 不同；f(3)=1 與 f(4)=5 不同。所有 x<y 的對都輸出不同（N1 以差的乘積非零核對），這是對有限 A 的完整檢查，依 S03，f 是單射。



S05 · implies操作前

f^{-1}(\{b\})=\{x\in A\mid f(x)=b\},\ b\in B

操作後

\{3\},\ \varnothing,\ \varnothing,\ \{1\},\ \{4\},\ \{2\}\quad(b=1,2,3,4,5,6)

條件：無

規則：image_preimage_def · 依賴：S01, image_preimage_def

葉節點依據：image_preimage_def + roster_membership + numeric_evaluation

對 B 的每個 b 列出纖維：b=1 時只有 f(3)=1，纖維 {3}；b=2、3 時沒有輸入對應，纖維為空；b=4 是 {1}；b=5 是 {4}；b=6 是 {2}。每個纖維至多一個元素；纖維大小總和 1+0+0+1+1+1=4=|A|（N8），每個輸入恰屬於一個纖維。



S06 · theorem_application操作前

|f^{-1}(\{b\})|\le 1\ \text{for all}\ b\in B

操作後

f\ \text{injective}

條件：無

規則：L_fiber · 依賴：S04, S05, L_fiber

葉節點依據：image_preimage_def + eq_refl_symm_trans + mko_injective_def

依引理 L_fiber，「每個纖維至多一個元素」與單射等價。S05 的纖維都至多一個元素，所以由纖維也得到 f 單射，與 S04 的逐對比較一致。這正是 MKO 敘述中的纖維等價形式。



S07 · implies操作前

f^{-1}(\{2\})=f^{-1}(\{3\})=\varnothing

操作後

f\ \text{injective but not surjective}

條件：無

規則：injective_surjective_def · 依賴：S05, S04, injective_surjective_def

葉節點依據：injective_surjective_def + image_preimage_def

陪域元素 2 與 3 的纖維是空的，沒有原像，所以 f 不是滿射；但 f 仍是單射（S04、S06）。MKO 第二段：單射可以漏掉陪域的元素，纖維大小可以是零或一。



S08 · implies操作前

g:\ (1,4),(2,6),(2,6),(3,4),(4,6)

操作後

g:A\to B\ \text{total};\ g(1)=4,\ g(2)=6,\ g(3)=4,\ g(4)=6

條件：無

規則：table_function · 依賴：G1, G2, table_function

葉節點依據：table_function + roster_membership

g 的表中 (2,6) 列了兩次。兩列完全相同，只是同一個有序對的重複列出（MKO 第一段），不構成「同一輸入配不同輸出」。四個輸入各有唯一輸出，輸出都在 B 中，所以 g 是總函數 A→B。



S09 · implies操作前

g(1)=4=g(3),\ 1\neq 3

操作後

g\ \text{not injective}

條件：無

規則：quantifier_negation · 依賴：S08, mko_injective_def, quantifier_negation

葉節點依據：quantifier_negation + exists_intro + mko_injective_def

單射的否定（量詞否定律加上 ¬(P⇒Q) ⇔ P∧¬Q）是：存在 x、y∈A 使 g(x)=g(y) 且 x≠y。取 x=1、y=3：g(1)=g(3)=4（N3）而 1≠3。這個碰撞見證就足以說明 g 不是單射。



S10 · implies操作前

\{(x,x')\mid x<x',\ g(x)=g(x')\}

操作後

\{(1,3),(2,4)\},\ \text{first}=(1,3)

條件：無

規則：lex_order · 依賴：S08, lex_order

葉節點依據：lex_order + case_analysis + numeric_evaluation

MKO 第三段：有限首碰撞先取 x<x′，再按 (x,x′) 字典序選首對。逐一比較六對：(1,2)：4 與 6 不同；(1,3)：4=4，碰撞；(1,4)：4 與 6 不同；(2,3)：6 與 4 不同；(2,4)：6=6，碰撞；(3,4)：4 與 6 不同（N4、N5）。碰撞集合為 {(1,3),(2,4)}；因 1<2，字典序首對是 (1,3)。



S11 · implies操作前

g^{-1}(\{b\}),\ b\in B

操作後

g^{-1}(\{4\})=\{1,3\},\ g^{-1}(\{6\})=\{2,4\},\ \text{others}\ \varnothing

條件：無

規則：image_preimage_def · 依賴：S08, image_preimage_def, L_fiber

葉節點依據：image_preimage_def + roster_membership + numeric_evaluation

g 的纖維：4 的纖維是 {1,3}，6 的纖維是 {2,4}，其餘 b=1、2、3、5 的纖維為空。大小總和 0+0+0+2+0+2=4=|A|（N9）。有兩個纖維含兩個元素，依 L_fiber 再次得到 g 不是單射，每個大小 2 的纖維對應一個碰撞。



S12 · implies操作前

g|_C,\ C=\{1,2\}

操作後

g|_C(1)=4\neq 6=g|_C(2),\ g|_C\ \text{injective}

條件：無

規則：restriction_def · 依賴：S08, G3, restriction_def, L_pairs_lt

葉節點依據：restriction_def + case_analysis + numeric_evaluation

限制到 C={1,2}：g|_C(1)=4、g|_C(2)=6。C 中 x<y 的對只有 (1,2)，而 4≠6（N6），依 L_pairs_lt，g|_C 是單射。MKO 第三段：限制後只比較 C 中的輸入，原函數不單射而限制後單射是可能的；兩個碰撞 (1,3)、(2,4) 都至少有一個輸入不在 C 中。



S13 · implies操作前

h:\ (2,6),\ (2,5)

操作後

h\ \text{is not a function}\ A\to B

條件：無

規則：table_function · 依賴：G2, table_function

葉節點依據：table_function + numeric_evaluation

h 的表中輸入 2 出現在 (2,6) 與 (2,5) 兩列，輸出 6≠5（N7）。同一輸入配不同輸出，所以 h 不是函數（MKO 第一段）。單射是對總函數定義的性質，因此「h 是否單射」這個問題不適用；正確的判定是「不是函數」，而不是「不是單射」。



S14 · implies操作前

f_0:\varnothing\to B

操作後

f_0\ \text{injective}

條件：無

規則：forall_intro · 依賴：G3, mko_injective_def, empty_set_def, forall_intro

葉節點依據：empty_set_def + forall_intro + mko_injective_def

空定義域時，單射條件是 ∀x,y∈∅ (f₀(x)=f₀(y)⇒x=y)。任取 x：x∈∅ 為假，前件為假的蘊涵為真，所以條件對每個 x、y 都成立；依 ∀引入，f₀ 是單射（MKO 假設 a2：空定義域的單射條件為真）。



S15 · implies操作前

\text{S01 to S14}

操作後

f\ \text{injective};\ g\ \text{not, first collision}\ (1,3);\ g|_C\ \text{injective};\ h\ \text{not a function};\ f_0\ \text{injective}

條件：無

規則：and_intro_elim · 依賴：S01, S04, S07, S08, S09, S10, S12, S13, S14

葉節點依據：and_intro_elim

彙整：f 是總函數且單射，纖維都至多一個元素，但 2、3 沒有原像（S04 到 S07）；g 是總函數（重複列無害），不單射，碰撞為 (1,3)、(2,4)，首碰撞 (1,3)（S08 到 S11）；g|_C 單射（S12）；h 不是函數（S13）；f₀:∅→B 單射（S14）。







## 局部子步與引理

S03.1 · equivalent操作前

\forall x<y:\ f(x)\neq f(y)

操作後

\forall x\neq y:\ f(x)\neq f(y)

條件：A\subseteq\mathbb{Z}

規則：case_analysis · 依賴：case_analysis, order_basics

葉節點依據：case_analysis + order_basics + eq_refl_symm_trans

⇐：x<y 推出 x≠y，所以由右式得左式。⇒：設 x≠y。由序的三分律，x<y 或 y<x。若 x<y，直接得 f(x)≠f(y)；若 y<x，得 f(y)≠f(x)，而「≠」是對稱的。兩種情況涵蓋 x≠y 的全部可能。這證得引理 L_pairs_lt（配合 S02）。



S06.1 · implies操作前

f\ \text{injective},\ x,x'\in f^{-1}(\{b\})

操作後

x=x'

條件：無

規則：mko_injective_def · 依賴：mko_injective_def, image_preimage_def

葉節點依據：mko_injective_def + image_preimage_def + eq_refl_symm_trans

⇒：設 f 單射，x、x′ 都在 b 的纖維中，則 f(x)=b=f(x′)，由等號的對稱與傳遞得 f(x)=f(x′)，單射給出 x=x′。所以纖維中任兩個元素相同，至多一個元素。



S06.2 · implies操作前

|f^{-1}(\{b\})|\le 1\ \forall b,\ f(x)=f(y)

操作後

x=y

條件：無

規則：image_preimage_def · 依賴：image_preimage_def

葉節點依據：image_preimage_def + forall_intro + eq_refl_symm_trans

⇐：設每個纖維至多一個元素，且 f(x)=f(y)。令 b=f(x)，則 x 與 y 都在 b 的纖維中；纖維至多一個元素，所以 x=y。這就是單射的定義。S06.1 與 S06.2 證得引理 L_fiber。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S04, S07, S10, S12, S13, S14, and_intro_elim — 目標 G：題目各項判定。足夠條件 H：所列各步的結論；H⇒G 只是合取，H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S14 · premise_audit · empty_set_def, forall_intro — 空真：沒有輸入，所以沒有碰撞可以否定單射。
- S13 · premise_audit · table_function — 一個輸入有兩個不同輸出就足以否定函數資格。
- S12 · premise_audit · restriction_def, L_pairs_lt — 需要列全 C 中的輸入對（只有一對）；不宣稱 g 本身因此單射。
- S11 · premise_audit · image_preimage_def, L_fiber — 只需一個大小超過 1 的纖維就足以否定單射；完整列出用來對照 S10。
- S10 · premise_audit · lex_order, S08, numeric_evaluation — 本稿採完整比較全部 6 對、列出全部碰撞後取字典序最小的稽核方法。數學上也可按字典序檢查，在排除所有更早對後於第一個碰撞停下；任意找到一個碰撞而未排除更早對則不足。這不改本稿完整列舉的既定程序。
- S09 · premise_audit · quantifier_negation, exists_intro, S08 — 一個碰撞見證就夠；它必須是 A 中兩個不同輸入。
- S08 · premise_audit · table_function — 重複列判定為無害，前提是兩列的輸出相同；若輸出不同，就像 h 一樣不是函數（S13）。
- S07 · premise_audit · injective_surjective_def, S05 — 一個沒有原像的陪域元素就足以否定滿射；這不影響單射的判定。
- S06.2 · premise_audit · image_preimage_def, forall_intro — x、y 是任意的，依 ∀引入得到對所有 x、y 的結論。
- S06.1 · premise_audit · mko_injective_def, image_preimage_def, eq_refl_symm_trans — 這是引理的「⇒」方向；反向在 S06.2。
- S06 · premise_audit · L_fiber, S05 — 引理在 S06.1、S06.2 證明；此步是第二條獨立路線，不依賴 S04。
- S05 · premise_audit · image_preimage_def, S01 — 需要對 B 的六個元素都列出；纖維大小總和等於 |A| 是一致性檢查。
- S04 · premise_audit · S03, case_analysis, numeric_evaluation — 必須比較全部 6 對；漏掉一對就不能下結論。結論只關於 f，不外推到其他函數。
- S03.1 · inverse_equivalence · case_analysis, order_basics, eq_refl_symm_trans — 兩向都有理由；需要 A 的元素可比較大小（整數標籤）。
- S03 · inverse_equivalence · L_pairs_lt — 引理兩向在 S03.1 證明。
- S02 · inverse_equivalence · contrapositive — 命題與其逆否命題等價，對每一對都雙向成立。
- S01 · premise_audit · table_function, G1, G2 — 三個條件（輸入輸出在範圍內、每個輸入出現、輸出唯一）都要核對；單射問題只對通過這一步的表才有意義。





## 錯誤控制與反例

單射不要求每個陪域元素都有原像MKO 指出的誤解之一是把單射當成每個陪域元素都有原像。f 的陪域元素 2、3 沒有原像（S07），f 仍是單射；「每個陪域元素都有原像」是滿射的條件。單射只要求纖維至多一個元素，零個也可以。

先確認總函數資格MKO 的另一個誤解是略過總函數資格。h 的輸入 2 對應 6 與 5，不是函數（S13），所以不能說「h 不是單射」；而 g 重複列出 (2,6) 並不破壞函數資格（S08）。判定單射前一定先做 S01、S08 這類檢查。

本稿從完整碰撞集合中選首碰撞一個碰撞見證就足以否定單射（S09），本稿求「首碰撞」採先列出全部 x<x′ 的碰撞對、再按字典序取最小的完整稽核；若使用字典序掃描，排除所有更早對後也可停在首個碰撞（S10）。若只隨便找到 (2,4) 就宣稱它是首碰撞，會錯過排在前面的 (1,3)。


- f 不是單射，因為陪域元素 2 沒有原像 → reject — 缺原像影響的是滿射；f 的六個輸入對輸出都不同，是單射。
- h 不是單射，因為 h(2) 有兩個值 → reject — h 根本不是函數；單射問題不適用，正確判定是「不是函數」。
- g 的表列出 (2,6) 兩次，所以 g 不是函數 → reject — 兩列完全相同，只是重複列出同一有序對；g 是總函數。
- g 不是單射，所以 g 限制到 C={1,2} 也不是單射 → reject — g|_C(1)=4≠6=g|_C(2)，限制後是單射。
- g 的首碰撞是 (2,4) → reject — 完整碰撞集合是 {(1,3),(2,4)}，字典序首對是 (1,3)。





## 結論與限制

f:(1,4),(2,6),(3,1),(4,5) 是總函數且單射：六個輸入對的輸出都不同，每個纖維至多一個元素；它不是滿射（2、3 沒有原像）。g 是總函數（重複的 (2,6) 無害）但不單射，碰撞對為 (1,3)、(2,4)，字典序首碰撞是 (1,3)；g 限制到 {1,2} 則是單射。h 的輸入 2 有兩個輸出，不是函數，單射問題不適用。空定義域的函數是單射。


- N1、N5 以「差的乘積非零」表示列出的各對輸出都不同（零乘積性質），只是對這些具體數字的重算。
- 本稿只處理有限整數標籤的表；L_pairs_lt 需要定義域可比較大小，對一般集合應直接使用 S02 的形式。





## 驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: dafc9b0a4b50798ff78dcf28638ea8cdec7b99bc6437f143ac45ff1db55d4b0b
- original source SHA-256: 2abb8f0cb47a609b84f38055e37ace578fef639ffbc99b0a564f7e91305f5af8
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-injective-01.json)