滿射與陪域覆蓋：值域、原像與陪域變更

目標與範圍

設 A={1,2,3,4,5}、B={1,2,3}，函數表 f：(1,2),(2,1),(3,3),(4,2),(5,1)。確認 f 是總函數 A→B，求值域 f[A] 與各原像，判定 f 是否滿射並找出 t=2 的首個原像；再把陪域換成 B2={1,2,3,4} 與 B3={1,2} 判定合法性與滿射性；最後處理 ∅→∅ 與 ∅→{7}。

在 MKO 的範圍內工作：明示定義域、陪域與有限總函數表。證明兩個一般小引理（f[A]⊆B；f 滿射 ⇔ f[A]=B），以完整核對判定本例，並示範陪域變更的合法性。結果只針對這張表，不外推到其他函數；不改動 canonical MKO 或英文 edition。

已知條件與符號

• function_def
• image_preimage_def
• set_extensionality
• exists_intro
• numeric_evaluation
• table_function

• G1 — 定義域 A={1,2,3,4,5}，宣告陪域 B={1,2,3}。
• G2 — 函數表 f：(1,2),(2,1),(3,3),(4,2),(5,1)（每列為 (輸入, 輸出)）。
• G3 — 替換陪域 B2={1,2,3,4}、B3={1,2}；目標 t=2；以及空函數 ∅→∅ 與 ∅→{7}。

• f[A] — 實際值域 {f(x) ∣ x∈A}
• B,\ B2,\ B3 — 宣告陪域與兩個替換陪域
• f^{-1}(\{t\}) — t 的原像集合 {x∈A ∣ f(x)=t}
• B\setminus f[A] — 未覆蓋的目標
• f_2 — 同一張表、陪域為 B2 的函數

規則與來源

• 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 有反函數。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• 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。
• 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_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_surjective_def · cited — 總函數 f:A→B 是滿射，當且僅當對每個 b∈B 都存在 x∈A 使 f(x)=b，也就是實際值域 f[A] 等於宣告陪域 B。滿射不要求原像唯一。 · mko-surjective
• 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。
• empty_set_def · prerequisite — 空集合：對每個 x，x∉∅。
• least_element · prerequisite — 非空有限整數集合有唯一的最小元素（逐一比較可得）。MKO 的「首個原像」指原像集合的數值最小元素；原像集合為空時答「不存在」。
• L_range_sub · lemma — 對任何總函數 f:A→B，f[A]⊆B。
• L_surj_range · lemma — 對總函數 f:A→B：f 是滿射 ⇔ f[A]=B。

逐步主鏈

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

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

f[A]=\{f(x)\mid x\in A\}

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

f[A]=\{1,2,3\}

f[A]\subseteq B

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

f^{-1}(\{1\})=\{2,5\},\ f^{-1}(\{2\})=\{1,4\},\ f^{-1}(\{3\})=\{3\}

b\in B=\{1,2,3\}

\forall b\in B\ \exists x\in A:\ f(x)=b

f[A]=\{1,2,3\}=B

f\ \text{surjective}

f(1)=f(4)=2,\ 1\neq 4

f\ \text{not injective, still surjective}

f^{-1}(\{2\})=\{1,4\}

\text{first preimage of}\ 2=\min\{1,4\}=1

f[A]=\{1,2,3\},\ B2=\{1,2,3,4\}

f[A]\subseteq B2,\ \text{so}\ f_2:A\to B2\ \text{is a total function}

B2\setminus f[A]

\{4\}\neq\varnothing,\ f_2^{-1}(\{4\})=\varnothing,\ f_2\ \text{not surjective}

f(3)=3,\ B3=\{1,2\}

3\notin B3,\ \text{so the table is not a function}\ A\to B3

\varnothing\to\varnothing

\text{surjective}

\varnothing\to\{7\}

\neg\exists x\in\varnothing:\ f(x)=7,\ \text{not surjective}

\text{S01 to S13}

f\ \text{surjective};\ f_2\ \text{not};\ B3\ \text{illegal};\ \varnothing\to\varnothing\ \text{surjective};\ \varnothing\to\{7\}\ \text{not}

局部子步與引理

y\in f[A]

y\in B

f\ \text{surjective}

f[A]=B

f[A]=B

f\ \text{surjective}

逐步反向審查

• S14 · sufficient_goal_reduction · S05, S06, S08, S10, S11, S12, S13, and_intro_elim — 目標 G：題目各項判定。足夠條件 H：所列各步的結論；H⇒G 只是合取，H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
• S13 · premise_audit · empty_set_def, quantifier_negation — 一個未覆蓋目標就足以否定；與 S12 的差別在陪域是否為空。
• S12 · premise_audit · empty_set_def, forall_intro — 空真：陪域沒有元素需要被覆蓋。
• S11 · premise_audit · table_function — 一個落在 B3 之外的輸出就足以否定合法性。
• S10 · premise_audit · L_surj_range, S09, numeric_evaluation — 一個未覆蓋目標就足以否定滿射（N6：|B2|−|f[A]|=1）。
• S09 · premise_audit · table_function, subset_def — 合法性只要求 f[A]⊆B2；它不涉及滿射。
• S08 · premise_audit · least_element, S04 — 需要原像集合完整（S04 檢查全部輸入）且非空。
• S07 · premise_audit · injective_surjective_def, S05 — 一個碰撞就否定單射；滿射的結論來自 S05，不受影響。
• S06.2 · premise_audit · image_preimage_def, forall_intro — b 是任意的，依 ∀引入得到對每個 b 的結論。
• S06.1 · premise_audit · mko_surjective_def, L_range_sub, set_extensionality — 這是引理的「⇒」方向；兩個包含缺一不可。
• S06 · premise_audit · L_surj_range, S02 — 引理兩向在 S06.1、S06.2 證明；這條路線不依賴 S05。
• S05 · premise_audit · S04, exists_intro, case_analysis, roster_membership, forall_intro — 需要 B 的每個元素都檢查到；每個 b 只需一個見證，不需要唯一。
• S04 · premise_audit · image_preimage_def, S01 — 需要逐一檢查全部五個輸入；大小總和等於 |A| 是一致性檢查。
• S03.1 · premise_audit · function_def, image_preimage_def, subset_def — 需要 f 是到 B 的函數；反方向 B⊆f[A] 一般不成立，不宣稱。
• S03 · premise_audit · L_range_sub — 引理在 S03.1 證明；它只給一個方向的包含。
• S02 · inverse_equivalence · image_preimage_def, set_extensionality — 兩個寫法有相同元素，依集合相等雙向成立。
• S01 · premise_audit · table_function — 滿射只對總函數有意義；三個資格條件都已核對。

錯誤控制與反例

值域不會自動等於陪域

MKO 指出的誤解之一是把值域自動當成陪域。同一張表的值域都是 {1,2,3}，陪域為 B 時滿射，陪域為 B2={1,2,3,4} 時不滿射（S10）。滿射是值域與「宣告」陪域的比較，必須先明示陪域。

多個原像不否定滿射

MKO 的另一個誤解是以多個原像否定滿射。2 有兩個原像 1、4，1 也有兩個原像 2、5；這使 f 不是單射（S07），但滿射只要求每個目標至少一個原像（S05）。

換陪域必須保留全部輸出

MKO 假設 a2：替換陪域須包含全部既有輸出。B3={1,2} 丟掉了仍出現的輸出 3，所以這張表不是 A→B3 的函數（S11）；不能用縮小陪域的方式「讓它變成滿射」。

• f 不是滿射，因為 2 有兩個原像 1 與 4 → reject — 滿射只要求每個目標至少一個原像；1、2、3 都有原像。
• f₂:A→{1,2,3,4} 是滿射，因為它的值域 {1,2,3} 就是陪域 → reject — 宣告陪域是 B2={1,2,3,4}，4 沒有原像。
• 把陪域改成 {1,2} 後，f 成為滿射 → reject — f(3)=3∉{1,2}，這張表不再是總函數，滿射問題不適用。
• 空函數 ∅→{7} 是滿射，因為找不到反例 → reject — 7 需要一個 x∈∅ 作原像，但 ∅ 沒有元素；7 本身就是未覆蓋目標。
• t=2 的首個原像是 4 → reject — 原像集合是 {1,4}，數值最小的是 1。

結論與限制

f:(1,2),(2,1),(3,3),(4,2),(5,1) 是總函數 A→B，f[A]={1,2,3}=B，所以 f 是滿射；它不是單射（f(1)=f(4)=2），但多個原像不影響滿射。t=2 的原像是 {1,4}，首個原像是 1。同一張表換成陪域 B2={1,2,3,4} 仍合法，但 4 沒有原像，不是滿射；換成 B3={1,2} 不合法，因為 f(3)=3∉B3。∅→∅ 是滿射，∅→{7} 不是。

• N3、N4 以「差的乘積非零」表示某數不等於每一個列出的值（零乘積性質），只是對這些具體數字的重算。
• 本稿不證明「有限集合間的滿射須 |A|≥|B|」等計數結論，也不處理無限定義域。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 5f960a2bdf50cfb476490d2df6deab5e3ce1ee98b23eb33287f6373c0377e4af
• original source SHA-256: 5f960a2bdf50cfb476490d2df6deab5e3ce1ee98b23eb33287f6373c0377e4af
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）