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

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

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

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



## 目標與範圍

設 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。





## 逐步主鏈

S01 · implies操作前

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

條件：無

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

葉節點依據：table_function + roster_membership

MKO 假設 a1：定義域、陪域與總函數都要明示。A 的五個輸入各恰出現一次，輸出 2、1、3、2、1 都在 B={1,2,3} 中，沒有輸入配到兩個輸出。所以 f 是總函數 A→B。



S02 · equivalent操作前

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

操作後

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

條件：無

規則：image_preimage_def · 依賴：S01, image_preimage_def, set_extensionality

葉節點依據：image_preimage_def + set_extensionality

值域是全部輸出所成的集合。五個輸出依序是 2、1、3、2、1；集合中重複值只算一次，所以 f[A]={1,2,3}。



S03 · theorem_application操作前

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

操作後

f[A]\subseteq B

條件：無

規則：L_range_sub · 依賴：S01, S02, L_range_sub

葉節點依據：function_def + image_preimage_def + subset_def

依引理 L_range_sub，任何總函數的值域都包含於陪域；本例 {1,2,3}⊆{1,2,3}。所以判定滿射時只需檢查反方向 B⊆f[A]。



S04 · implies操作前

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

操作後

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

條件：無

規則：image_preimage_def · 依賴：S01, image_preimage_def

葉節點依據：image_preimage_def + roster_membership + numeric_evaluation

逐一列出 B 中每個目標的原像：輸出為 1 的輸入是 2、5；輸出為 2 的是 1、4；輸出為 3 的是 3。三個原像集合互斥，大小 2+2+1=5=|A|（N1），每個輸入恰屬於其中一個。



S05 · implies操作前

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

操作後

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

條件：無

規則：mko_surjective_def · 依賴：S04, mko_surjective_def, exists_intro, case_analysis

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

任取 b∈B。B 以列舉給出，所以 b=1、2 或 3。b=1 時見證 x=2；b=2 時見證 x=1；b=3 時見證 x=3（S04）。三種情況涵蓋 B 的全部元素，每種都有原像；依 ∃引入與 ∀引入，f 是滿射。



S06 · theorem_application操作前

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

操作後

f\ \text{surjective}

條件：無

規則：L_surj_range · 依賴：S02, S05, L_surj_range

葉節點依據：image_preimage_def + set_extensionality + mko_surjective_def

第二條路線：依引理 L_surj_range，f 是滿射當且僅當 f[A]=B。S02 得 f[A]={1,2,3}，正是 B，所以 f 是滿射，與 S05 的逐點檢查一致。



S07 · implies操作前

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

操作後

f\ \text{not injective, still surjective}

條件：無

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

葉節點依據：injective_surjective_def + numeric_evaluation

f(1)=f(4)=2 而 1≠4（N5），所以 f 不是單射；同樣 f(2)=f(5)=1。但 S05 已證 f 是滿射。MKO 敘述明示：滿射不要求原像唯一；多個輸入映到同一目標不會破壞滿射。



S08 · implies操作前

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

操作後

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

條件：f^{-1}(\{2\})\neq\varnothing

規則：least_element · 依賴：S04, G3, least_element

葉節點依據：least_element + order_basics + numeric_evaluation

MKO 第二段：首個原像指有限整數資料中數值最小的原像。t=2 的原像集合 {1,4} 非空，最小元素是 1（N2），所以首個原像是 1。它來自完整的原像集合，不是表中第一個碰到的列。



S09 · implies操作前

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}

條件：無

規則：table_function · 依賴：S02, G3, table_function, subset_def

葉節點依據：table_function + subset_def

MKO 假設 a2：更換陪域時，新陪域必須包含全部既有輸出，同一份表才仍是合法總函數。輸出 1、2、3 都在 B2 中，所以同一張表定義總函數 f₂:A→B2。



S10 · implies操作前

B2\setminus f[A]

操作後

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

條件：無

規則：L_surj_range · 依賴：S09, S02, L_surj_range

葉節點依據：image_preimage_def + set_operations_def + numeric_evaluation

未覆蓋的目標是 B2∖f[A]={4}：五個輸出 2、1、3、2、1 都不等於 4（N3），所以 4 沒有原像，首個原像「不存在」。f₂[A]={1,2,3}≠B2，依 L_surj_range，f₂ 不是滿射。同一張輸出表，換了陪域，滿射性就改變（MKO 第三段）。



S11 · implies操作前

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

操作後

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

條件：無

規則：table_function · 依賴：S01, G3, table_function

葉節點依據：table_function + roster_membership + numeric_evaluation

若把陪域換成 B3={1,2}：f(3)=3 而 3∉B3（N4），違反「輸出在陪域中」的條件，所以這張表不是 A→B3 的總函數。不能為了讓值域「等於」陪域而丟掉仍出現的輸出 3；對 B3 根本不能問滿射。



S12 · implies操作前

\varnothing\to\varnothing

操作後

\text{surjective}

條件：無

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

葉節點依據：empty_set_def + forall_intro + mko_surjective_def

空函數 ∅→∅：滿射條件是 ∀b∈∅ ∃x∈∅ f(x)=b。任取 b：b∈∅ 為假，蘊涵為真；依 ∀引入，條件成立，所以 ∅→∅ 是滿射（MKO 第三段）。



S13 · implies操作前

\varnothing\to\{7\}

操作後

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

條件：無

規則：quantifier_negation · 依賴：G3, mko_surjective_def, empty_set_def, quantifier_negation

葉節點依據：empty_set_def + quantifier_negation + mko_surjective_def

空函數 ∅→{7}：7∈{7} 需要某個 x∈∅ 使 f(x)=7，但 ∅ 沒有元素，所以 ¬∃x∈∅ f(x)=7。7 是未覆蓋目標，依量詞否定律，∀b∈{7} ∃x 的條件失敗，∅→{7} 不是滿射。



S14 · implies操作前

\text{S01 to S13}

操作後

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

條件：無

規則：and_intro_elim · 依賴：S05, S06, S07, S08, S10, S11, S12, S13

葉節點依據：and_intro_elim

彙整：f:A→B 是滿射，f[A]=B，雖然不是單射；t=2 的首個原像是 1（S05 到 S08）。換成 B2 合法但不滿射，4 未覆蓋（S09、S10）；換成 B3 不合法（S11）。∅→∅ 是滿射，∅→{7} 不是（S12、S13）。







## 局部子步與引理

S03.1 · implies操作前

y\in f[A]

操作後

y\in B

條件：無

規則：function_def · 依賴：function_def, image_preimage_def, subset_def

葉節點依據：function_def + image_preimage_def + subset_def + exists_elim

設 y∈f[A]。依像的定義，有 x∈A 使 y=f(x)；依函數定義，f(x)∈B，所以 y∈B。y 是任意的，依子集定義 f[A]⊆B。這證得引理 L_range_sub。



S06.1 · implies操作前

f\ \text{surjective}

操作後

f[A]=B

條件：無

規則：set_extensionality · 依賴：mko_surjective_def, image_preimage_def, L_range_sub, set_extensionality

葉節點依據：mko_surjective_def + image_preimage_def + set_extensionality

⇒：設 f 滿射。任取 b∈B，有 x∈A 使 f(x)=b，所以 b∈f[A]，得 B⊆f[A]。另由 L_range_sub，f[A]⊆B。兩個包含合起來，依集合相等 f[A]=B。



S06.2 · implies操作前

f[A]=B

操作後

f\ \text{surjective}

條件：無

規則：image_preimage_def · 依賴：image_preimage_def, mko_surjective_def

葉節點依據：image_preimage_def + forall_intro + mko_surjective_def

⇐：設 f[A]=B。任取 b∈B，則 b∈f[A]，依像的定義有 x∈A 使 f(x)=b。b 是任意的，所以 f 是滿射。S06.1 與 S06.2 證得引理 L_surj_range。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-surjective-01.json)