# 雙射：以纖維概況判定給定函數，並與「是否存在某個雙射」分開

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

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

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



## 目標與範圍

設 A={1,2,3}、B={4,5,6}，函數 f、g:A→B 由表給出：f(1)=5、f(2)=6、f(3)=4；g(1)=4、g(2)=4、g(3)=6。先對一般總函數證明「雙射 ⇔ 每個 b∈B 的纖維恰有一個元素」，再按陪域 4、5、6 的順序列出 f 與 g 的完整纖維概況，判定 f 是雙射、g 既非單射也非滿射。最後回答另一類問題「是否存在某個雙射」：A→B 存在（f 即是）、{1,2,3}→{4,5} 不存在、∅→∅ 恰有一個空雙射。

纖維刻畫（S03 至 S05）對任意集合上的總函數證明；其餘都是 MKO 假設 a1、a2 下的有限集合題。存在性方向：A→B 以明確見證 f 回答，{1,2,3}→{4,5} 的不存在在子步中直接證明，一般的「有限集合間存在雙射 ⇔ 元素個數相同」取自前置規則 finite_counting_basics，本稿不另證。不處理無限基數；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- injective_surjective_def
- image_preimage_def
- set_builder
- finite_counting_basics
- numeric_evaluation


- G1 — A={1,2,3}、B={4,5,6}；f:A→B 為 f(1)=5、f(2)=6、f(3)=4。
- G2 — g:A→B 為 g(1)=4、g(2)=4、g(3)=6；陪域仍宣告為 B={4,5,6}。
- G3 — C={4,5}；問題：是否存在雙射 A→C。
- G4 — MKO 假設 a1：判定給定函數與詢問是否存在某個雙射是不同問題。a2：存在性題限定有限集合，大小為非負整數；兩邊大小皆為零時有唯一的空雙射。


- f,g:A\to B — 兩個給定的總函數
- f^{-1}(\{b\}) — b 的纖維 {a∈A ∣ f(a)=b}；記號不預設 f 可逆
- |S| — 有限集合 S 的元素個數
- A=\{1,2,3\},\ B=\{4,5,6\},\ C=\{4,5\} — 定義域與兩個陪域
- \varnothing — 空集合





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- 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。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- 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。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- 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)。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- mko_bijective_def · cited — 總函數 f:A→B 為雙射，當且僅當它同時單射與滿射；等價地，每個 b∈B 的纖維恰有一個元素。對有限集合，存在某個 A→B 的雙射當且僅當 |A|=|B|；基數相等不保證任意給定 f 都是雙射。 · mko-bijective
- fiber_def · prerequisite — 纖維：對函數 f:A→B 與 b∈B，b 的纖維是原像 f^{-1}({b})={a∈A ∣ f(a)=b}；它對每個函數都有定義，可以是空集合。
- count_maps · prerequisite — 計數（乘法原理）：若 |A|=m、|B|=n，則 A→B 的函數共有 n^m 個；若 m=n，其中雙射共有 n! 個。
- L_inj_fiber · lemma — 對總函數 f:A→B：f 單射 ⇔ 每個 b∈B 的纖維至多一個元素。
- L_surj_fiber · lemma — 對總函數 f:A→B：f 滿射 ⇔ 每個 b∈B 的纖維至少一個元素。
- L_no_inj_3_2 · lemma — 任何函數 h:{1,2,3}→{4,5} 都不是單射。





## 逐步主鏈

S01 · definition操作前

f,g\ \text{given by tables on}\ A=\{1,2,3\}

操作後

f,g:A\to B\ \text{total functions},\ B=\{4,5,6\}

條件：無

規則：function_def · 依賴：G1, G2

葉節點依據：function_def

先確認題目給的確實是總函數：在 f 的表中，1、2、3 各出現恰好一次，值 5、6、4 都在 B 中；g 的表也一樣，值 4、4、6 都在 B 中。陪域是題目宣告的 B={4,5,6}，不是由表中出現的值反推，所以 g 從未取到的 5 仍屬於陪域。



S02 · definition操作前

b\in B

操作後

f^{-1}(\{b\})=\{a\in A\mid f(a)=b\}

條件：無

規則：fiber_def · 依賴：S01

葉節點依據：fiber_def + image_preimage_def + set_builder

對陪域中的每個目標 b 定義其纖維，即被 f 送到 b 的全部輸入。完整的纖維概況按陪域目標排列，包含沒有原像的目標（空纖維）。f^{-1}({b}) 只是原像記號，對不可逆的函數也有意義。



S03 · equivalent操作前

f\ \text{injective}

操作後

\forall b\in B:\ |f^{-1}(\{b\})|\le 1

條件：無

規則：L_inj_fiber · 依賴：S02

葉節點依據：injective_surjective_def + set_builder + eq_refl_symm_trans

依引理 L_inj_fiber，把單射改寫成纖維的條件：每個纖維至多一個元素。引理的兩個方向在 S03.1 與 S03.2 證明，對任意集合上的總函數成立，不需要有限性。



S04 · equivalent操作前

f\ \text{surjective}

操作後

\forall b\in B:\ |f^{-1}(\{b\})|\ge 1

條件：無

規則：L_surj_fiber · 依賴：S02

葉節點依據：injective_surjective_def + set_builder

依引理 L_surj_fiber，把滿射改寫成：每個纖維至少一個元素（非空）。證明在 S04.1。



S05 · equivalent操作前

f\ \text{bijective}

操作後

\forall b\in B:\ |f^{-1}(\{b\})|=1

條件：無

規則：mko_bijective_def · 依賴：S03, S04

葉節點依據：injective_surjective_def + and_intro_elim + order_basics

雙射的定義是單射且滿射。以 S03、S04 的等價分別替換兩個合取項，得到：每個 b 的纖維同時「至多一個元素」且「至少一個元素」，恰好就是「恰有一個元素」。這個推論不需要先假設纖維有限，也不把一般函數的纖維大小預設為非負整數。這就是 MKO 所說的等價刻畫。



S06 · equivalent操作前

f^{-1}(\{4\}),\ f^{-1}(\{5\}),\ f^{-1}(\{6\})

操作後

\{3\},\ \{1\},\ \{2\}

條件：無

規則：set_builder · 依賴：G1, S02

葉節點依據：set_builder + set_extensionality + numeric_evaluation

逐一掃描 A 的三個元素：f(1)=5、f(2)=6、f(3)=4。目標 4 只由 3 達到，目標 5 只由 1 達到，目標 6 只由 2 達到。A 是有限集合，三個元素全部檢查過，所以每個纖維都已完整求出。f 的纖維概況（按 4、5、6）是 (1,1,1)。



S07 · implies操作前

|f^{-1}(\{4\})|=|f^{-1}(\{5\})|=|f^{-1}(\{6\})|=1

操作後

f\ \text{bijective}

條件：B=\{4,5,6\}

規則：mko_bijective_def · 依賴：S05, S06

葉節點依據：mko_bijective_def + forall_intro + and_intro_elim

B 恰有 4、5、6 三個目標，S06 顯示三個纖維都恰有一個元素，所以「每個 b∈B 的纖維恰有一個元素」成立；依 S05，f 是雙射。



S08 · equivalent操作前

g^{-1}(\{4\}),\ g^{-1}(\{5\}),\ g^{-1}(\{6\})

操作後

\{1,2\},\ \varnothing,\ \{3\}

條件：無

規則：set_builder · 依賴：G2, S02

葉節點依據：set_builder + set_extensionality + numeric_evaluation

對 g 做同樣的掃描：g(1)=4、g(2)=4、g(3)=6。目標 4 由 1 與 2 達到，目標 6 只由 3 達到，目標 5 沒有任何輸入達到。g 的完整纖維概況（按 4、5、6）是 (2,0,1)，其中空纖維必須列出。



S09 · implies操作前

|g^{-1}(\{4\})|=2

操作後

g\ \text{not injective}

條件：無

規則：L_inj_fiber · 依賴：S03, S08

葉節點依據：L_inj_fiber + contrapositive

纖維 g^{-1}({4})={1,2} 有兩個元素，違反「每個纖維至多一個元素」；依 L_inj_fiber 的 ⇒ 方向取逆否，g 不是單射。具體見證：g(1)=g(2)=4 而 1≠2。



S10 · implies操作前

g^{-1}(\{5\})=\varnothing

操作後

g\ \text{not surjective}

條件：5\in B

規則：L_surj_fiber · 依賴：S04, S08

葉節點依據：L_surj_fiber + contrapositive

5 屬於宣告的陪域 B，但它的纖維是空集合；依 L_surj_fiber，g 不是滿射。所以 g 兩個條件都不滿足，屬於「兩者皆非」一類。



S11 · implies操作前

|A|=|B|=3,\ g\ \text{not bijective}

操作後

\neg\,\forall\varphi:A\to B\ (\varphi\ \text{bijective})

條件：無

規則：quantifier_negation · 依賴：G1, S09

葉節點依據：quantifier_negation + exists_intro

A 與 B 各有三個元素，大小相等；但 S09 已證 g 不是雙射。所以「大小相等的有限集合之間，每個函數都是雙射」這個全稱命題有反例 g，為假。這正是 MKO 假設 a1：判定給定函數不能只看兩個集合的大小。



S12 · implies操作前

|A|=3,\ |C|=2

操作後

\neg\exists h:A\to C\ \text{bijective}

條件：無

規則：L_no_inj_3_2 · 依賴：G3

葉節點依據：injective_surjective_def + contrapositive

轉到存在性問題。依引理 L_no_inj_3_2，任何 h:A→C 都不是單射，因此沒有一個是雙射。這與前置規則 finite_counting_basics（3≠2）一致，但這裡在 S12.1 至 S12.3 直接證明，不依賴該一般定理。



S13 · implies操作前

f:A\to B\ \text{bijective}

操作後

\exists\varphi:A\to B\ \text{bijective}

條件：無

規則：exists_intro · 依賴：S07

葉節點依據：exists_intro

存在性問題「A→B 有沒有某個雙射」由明確見證回答：S07 已證 f 是雙射，所以存在。這與 finite_counting_basics（|A|=|B|=3）一致。注意這個答案只說「有某個」，對 g 是否雙射沒有任何結論。



S14 · implies操作前

|A|=|B|=3

操作後

3^3=27\ \text{functions},\ 3!=6\ \text{bijections}

條件：無

規則：count_maps · 依賴：G1

葉節點依據：count_maps + numeric_evaluation

依乘法原理，A→B 共有 3^3=27 個函數，其中雙射 3!=6 個，所以有 21 個函數不是雙射，g 是其中之一。大小相等只保證「有」雙射，並不使大多數函數成為雙射。



S15 · implies操作前

\varnothing\to\varnothing

操作後

\varepsilon=\varnothing\ \text{is the unique bijection}\ \varnothing\to\varnothing

條件：無

規則：injective_surjective_def · 依賴：G4, function_def

葉節點依據：function_def + injective_surjective_def + cartesian_product_def + forall_intro

函數 ∅→∅ 是 ∅×∅=∅ 的子集合，且每個定義域元素恰有一個值；定義域沒有元素，條件空真，所以唯一的子集合 ∅ 就是唯一的函數，記為 ε。單射空真（沒有兩個輸入可比較），滿射也空真（陪域沒有需要達到的目標），因此 ε 是雙射；按纖維看，陪域沒有目標，「每個纖維恰有一個元素」同樣空真。這對應 a2：|∅|=0=|∅| 時有唯一的空雙射。



S16 · implies操作前

\text{S07, S09, S10, S12, S13, S15}

操作後

f\ \text{bijective};\ g\ \text{neither};\ \exists\,A\to B;\ \nexists\,A\to C;\ \exists!\,\varnothing\to\varnothing

條件：無

規則：and_intro_elim · 依賴：S07, S09, S10, S12, S13, S15

葉節點依據：and_intro_elim

把結果分成兩類問題整理。給定函數：f 的纖維概況 (1,1,1)，是雙射；g 的纖維概況 (2,0,1)，既非單射也非滿射。存在性：A→B 有雙射（見證 f），A→C 沒有，∅→∅ 恰有一個。







## 局部子步與引理

S03.1 · implies操作前

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

操作後

a=a'

條件：無

規則：injective_surjective_def · 依賴：S02, injective_surjective_def, set_builder

葉節點依據：injective_surjective_def + set_builder + eq_refl_symm_trans

（⇒）設 f 單射，a、a′ 都在 b 的纖維中。依集合建構式，f(a)=b 且 f(a′)=b，所以 f(a)=f(a′)；單射給出 a=a′。纖維中任兩個元素都相等，故至多一個元素。



S03.2 · implies操作前

\forall b:\ |f^{-1}(\{b\})|\le 1,\ f(a)=f(a')

操作後

a=a'

條件：無

規則：injective_surjective_def · 依賴：S02, set_builder, function_def

葉節點依據：function_def + set_builder + injective_surjective_def

（⇐）設每個纖維至多一個元素，且 f(a)=f(a′)。令 b=f(a)，因 f 是 A→B 的函數，b∈B。依集合建構式 a 與 a′ 都在 b 的纖維中；該纖維至多一個元素，所以 a=a′，即 f 單射。S03.1 與 S03.2 合起來證得引理 L_inj_fiber。



S04.1 · equivalent操作前

\exists a\in A:\ f(a)=b

操作後

f^{-1}(\{b\})\neq\varnothing

條件：無

規則：set_builder · 依賴：S02, injective_surjective_def, set_builder

葉節點依據：set_builder + injective_surjective_def

滿射的定義是：每個 b∈B 都有某個 a∈A 使 f(a)=b。對固定的 b，「有某個 a 使 f(a)=b」恰好表示集合 {a∈A ∣ f(a)=b} 有元素，即纖維非空。對所有 b 取全稱，得到引理 L_surj_fiber。



S12.1 · case_split操作前

h:\{1,2,3\}\to\{4,5\}

操作後

h(1)=h(2)\ \lor\ h(1)\neq h(2)

條件：無

規則：case_analysis · 依賴：G3, function_def

葉節點依據：case_analysis + injective_surjective_def

任取函數 h:A→C，分兩種情形，兩者涵蓋一切可能。情形一 h(1)=h(2)：因 1≠2，h 已不是單射，這個情形完成。情形二 h(1)≠h(2) 在 S12.2、S12.3 處理。



S12.2 · implies操作前

h(1)\neq h(2),\ h(1),h(2)\in\{4,5\}

操作後

\{h(1),h(2)\}=\{4,5\}

條件：無

規則：case_analysis · 依賴：S12.1, G3

葉節點依據：case_analysis + set_extensionality

情形二：h(1) 是 4 或 5。若 h(1)=4，則 h(2)≠4，而 h(2)∈{4,5}，所以 h(2)=5；若 h(1)=5，同理 h(2)=4。兩個子情形都得到 {h(1),h(2)}={4,5}。



S12.3 · implies操作前

h(3)\in\{4,5\}=\{h(1),h(2)\}

操作後

h(3)=h(1)\ \lor\ h(3)=h(2)

條件：無

規則：injective_surjective_def · 依賴：S12.2

葉節點依據：injective_surjective_def + case_analysis + forall_intro

h(3) 也在 {4,5}={h(1),h(2)} 中，所以 h(3)=h(1) 或 h(3)=h(2)；而 3≠1、3≠2，兩種都違反單射。情形一（S12.1）與情形二都得到 h 不是單射，h 又是任意取的，S12.1 至 S12.3 證得引理 L_no_inj_3_2。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S07, S09, S10, S12, S13, S15, and_intro_elim — 目標 G 是 goal 中的全部判定。足夠條件 H 是各子結論的合取，每一項都已由前面的步驟從已知正向證成；H⇒G 只用合取引入，沒有把 G 當作前提。
- S15 · premise_audit · function_def, injective_surjective_def, cartesian_product_def, forall_intro — 所有條件都是對空集合的全稱，因此空真；唯一性來自 ∅×∅ 只有一個子集合。
- S14 · premise_audit · count_maps, numeric_evaluation — 計數規則是前置知識，本稿不證；這一步只作說明，主結論 S07、S09 至 S13 不依賴它。
- S13 · premise_audit · S07, exists_intro — 存在引入只需一個見證；反向（存在某個雙射 ⇒ 每個函數都是雙射）不成立，S11 已給反例。
- S12.3 · premise_audit · injective_surjective_def, case_analysis, forall_intro — 兩個情形各自推出同一結論，h 沒有附加假設，所以可推廣到所有 h。
- S12.2 · premise_audit · case_analysis, set_extensionality — 用到的是 C 只有兩個元素；兩個子情形窮盡 h(1) 的可能值。反向不需要。
- S12.1 · premise_audit · case_analysis, injective_surjective_def — 兩個情形是「相等或不相等」，互補且窮盡；情形一直接由單射定義否定。
- S12 · premise_audit · L_no_inj_3_2, injective_surjective_def — 雙射必須單射；既然沒有單射的 h，也就沒有雙射。這裡不宣稱 A→C 沒有滿射（例如 1↦4、2↦5、3↦5 就是滿射）。
- S11 · premise_audit · S09, quantifier_negation, exists_intro — 一個明確反例就足以否定全稱命題；本步不宣稱大多數函數都不是雙射（那是 S14 的計數）。
- S10 · premise_audit · L_surj_fiber, S08, S01 — 結論依賴 5∈B；若有人把陪域縮成 {4,6}，那是另一個函數，不影響本題對宣告陪域的判定。
- S09 · premise_audit · L_inj_fiber, contrapositive, S08 — 只要一個纖維大於一就足以否定單射；本步不宣稱其他纖維的任何性質。
- S08 · inverse_equivalence · set_builder, set_extensionality, G2 — A 的三個元素都已對每個目標檢查；列出的元素滿足條件，其餘不滿足，集合逐元素相同。
- S07 · premise_audit · S05, S06, G1 — 需要的是陪域中的每個目標都被檢查到；B 的三個元素都在 S06 中出現，沒有遺漏的目標。本步只用 S05 的 ⇐ 方向。
- S06 · inverse_equivalence · set_builder, set_extensionality, G1 — 每個列出的元素都滿足 f(a)=b，A 中其餘兩個元素都已驗證不滿足；依集合外延性，兩邊的集合相同，雙向成立。
- S05 · inverse_equivalence · S03, S04, and_intro_elim, order_basics — 每個合取項都換成等價的條件，合取保持等價；對整數，n≤1 且 n≥1 ⇔ n=1 雙向成立（反對稱與自反）。
- S04.1 · inverse_equivalence · set_builder, injective_surjective_def — 集合建構式的成員條件本身是雙向的：纖維中的元素就是所需的 a，所需的 a 也就是纖維中的元素。
- S04 · inverse_equivalence · L_surj_fiber — S04.1 的等價對每個 b 雙向成立，對所有 b 同時取全稱後仍雙向成立。
- S03.2 · premise_audit · function_def, set_builder, injective_surjective_def — 關鍵是 b=f(a) 屬於 B，這樣才能套用「每個 b∈B 的纖維」這個假設；這由 f 是總函數保證。
- S03.1 · premise_audit · injective_surjective_def, set_builder, eq_refl_symm_trans — 只用到單射定義與等號的對稱、傳遞；這是單向推論，反向由 S03.2 另行證明。
- S03 · inverse_equivalence · L_inj_fiber — ⇒ 由 S03.1 證明，⇐ 由 S03.2 證明；兩個方向都有理由，所以是等價。
- S02 · premise_audit · fiber_def, image_preimage_def — 只是命名一個對所有函數都存在的集合，沒有宣稱任何纖維非空或只有一個元素。
- S01 · premise_audit · G1, G2, function_def — 此步只讀表並核對函數定義的兩個要求（每個輸入有值、值唯一），不推出新事實。若把陪域改成值的集合，後面的滿射判定會改變，所以陪域必須照題目宣告。





## 錯誤控制與反例

大小相等不等於給定函數是雙射MKO 的誤解是由 |A|=|B| 直接判定給定 f 為雙射。g 就是反例：|A|=|B|=3，但 g(1)=g(2)=4 且 5 無原像。A→B 的 27 個函數中只有 6 個是雙射（S14）。大小相等只回答「是否存在某個雙射」（S13），判定給定函數必須看它的纖維。

只查一個條件不夠只驗單射或只驗滿射會漏判。k:{1,2}→{4,5,6}，k(1)=4、k(2)=5 是單射，但 6 的纖維是空的，不是滿射。對大小相等的有限集合，單射與滿射確實互相推出，但那是需要另行證明的定理，不能直接假設；在無限集合上它也不成立，例如 ℕ→ℕ 的 n↦n+1 是單射而非滿射。本稿對 f 經由纖維概況同時核對兩個條件。

空纖維不可漏若只從 g 的表列出出現過的值，會得到 4↦{1,2}、6↦{3}，而遺漏目標 5。纖維概況必須按宣告的陪域逐一列出，5 的空纖維正是 g 不滿射的證據（S10）。


- |A|=|B|=3，所以 g 是雙射 → reject — g(1)=g(2)=4 且 1≠2，g 不是單射；5 的纖維為空，g 不是滿射。
- k:{1,2}→{4,5,6}，k(1)=4、k(2)=5 是單射，所以是雙射 → reject — 6 的纖維是空集合，k 不是滿射；而且 |{1,2}|=2≠3，根本不存在 {1,2}→{4,5,6} 的雙射。
- g 不是雙射，所以 A→B 之間不存在雙射 → reject — 給定函數與存在性是不同問題；f 就是一個 A→B 的雙射（S07、S13）。
- 空集合之間沒有函數，所以 ∅→∅ 談不上雙射 → reject — 空函數 ε=∅ 是 ∅→∅ 的唯一函數，單射與滿射皆空真，所以它是雙射（S15）。





## 結論與限制

f 的纖維概況（按 4、5、6）為 (1,1,1)，所以 f 是雙射；g 的纖維概況為 (2,0,1)，g 既非單射（g(1)=g(2)）也非滿射（5 無原像），雖然 |A|=|B|=3。一般地，總函數是雙射當且僅當每個纖維恰有一個元素（S05）。存在性另成一題：A→B 存在雙射（f），{1,2,3}→{4,5} 不存在任何雙射（實際上沒有單射），∅→∅ 恰有一個空雙射。


- 一般結論「有限集合間存在雙射 ⇔ 元素個數相同」取自前置規則 finite_counting_basics，本稿未證；本稿只以見證 f 回答 A→B，並直接證明 3 元素集合到 2 元素集合沒有單射。
- 計數規則 count_maps（27 與 6）為前置知識，S14 只作說明，主結論不依賴它。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3cc1ae7f0a2851556bf4390ecba06ec72251dbf8678c4accbd7061d54a693764
- original source SHA-256: 3cc1ae7f0a2851556bf4390ecba06ec72251dbf8678c4accbd7061d54a693764
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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