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

目標與範圍

設 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} 都不是單射。

逐步主鏈

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

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

b\in B

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

f\ \text{injective}

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

f\ \text{surjective}

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

f\ \text{bijective}

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

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

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

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

f\ \text{bijective}

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

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

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

g\ \text{not injective}

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

g\ \text{not surjective}

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

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

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

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

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

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

|A|=|B|=3

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

\varnothing\to\varnothing

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

\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

局部子步與引理

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

a=a'

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

a=a'

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

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

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

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

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

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

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

h(3)=h(1)\ \lor\ h(3)=h(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、反控制與修訂記錄）