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

目標與範圍

設 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}) 至多有一個元素。

逐步主鏈

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

\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)

\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)

(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}

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)

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

f\ \text{injective}

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

f\ \text{injective but not surjective}

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

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

g\ \text{not injective}

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

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

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

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

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

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

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

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

f_0:\varnothing\to B

f_0\ \text{injective}

\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}

局部子步與引理

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

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

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

x=x'

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

x=y

逐步反向審查

• 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、反控制與修訂記錄）