# 函數映射：判定對應是否為函數，並分辨陪域、值域與圖形

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

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

derivation-mko-function-mapping-01 · production-20261019-adopted-96



## 目標與範圍

設 X={−2,−1,0,1,2}、Y={0,1,2,3,4,5}，f:X→Y，f(x)=x²。證明 f 是函數；算出值域 f(X)={0,1,4} 並說明 f(X)≠Y；寫出圖形 Γ_f；說明把陪域改成 {0,1,4} 會得到不同的函數。再判定兩個非例：反向規則 s(y)=「X 中滿足 x²=y 的 x」不是 Y→X 的函數；g(x)=x+4 不是 X→Y 的函數。

只處理明示的有限集合 X、Y 之間的純數學總函數（MKO 假設 a1、a2）。有限集合上的全稱語句以完整窮舉核對。不給出部分函數的形式定義，不綁定 Lean 定理 function_total_unique，也不處理程式語意；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- image_preimage_def
- injective_surjective_def
- cartesian_product_def
- finite_forall


- G1 — X={−2,−1,0,1,2}，Y={0,1,2,3,4,5}，兩者都是明示的整數集合（假設 a1）。
- G2 — f:X→Y 由規則 f(x)=x² 給出。
- G3 — 兩個比較用的規則：s 從 Y 到 X，s(y) 為「X 中滿足 x²=y 的 x」；g 從 X 到 Y，g(x)=x+4。


- X,\ Y — 定義域與陪域
- f(X) — 值域：實際輸出之集
- \Gamma_f — 圖形：有序對 (x,f(x)) 之集
- f_1 — 同一規則、陪域改為 {0,1,4} 的函數
- s,\ g — 兩個要判定的對應規則





## 規則與來源


- 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 有反函數。
- 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。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- mko_function_def · cited — 函數 f:X→Y 對 X 中每一個輸入指定 Y 中唯一一個輸出；陪域 Y 不必等於實際值域。 · mko-function-mapping
- finite_forall · prerequisite — 有限列舉集合上的量詞：若 X 以列舉給出，則 ∀x∈X, P(x) 等價於每個列出的元素都滿足 P；∃x∈X, P(x) 等價於至少一個列出的元素滿足 P。
- graph_def · prerequisite — 函數圖形：f:X→Y 的圖形是 Γ_f={(x,f(x)) ∣ x∈X}，它是 X×Y 的子集合。
- L_no_root_2 · lemma — X 中沒有 x 使 x²=2。





## 逐步主鏈

S01 · definition操作前

\text{rule }x\mapsto x^2

操作後

f:X\to Y,\ X=\{-2,-1,0,1,2\},\ Y=\{0,1,2,3,4,5\},\ f(x)=x^2

條件：無

規則：def_intro · 依賴：G1, G2

葉節點依據：def_intro + mko_function_def

宣告 f:X→Y 同時給出三項資料：定義域 X、陪域 Y，以及對應規則 x↦x²。依 MKO，函數的核心是「每個允許的輸入對應唯一輸出」這條規則，而不是畫出的曲線；X、Y 是明示的集合（假設 a1）。



S02 · equivalent操作前

f:X\to Y\ \text{is a function}

操作後

\forall x\in X:\ x^2\in Y\ \land\ \forall y,y'\ (y=x^2\land y'=x^2\Rightarrow y=y')

條件：無

規則：mko_function_def · 依賴：S01, mko_function_def

葉節點依據：mko_function_def + function_def + def_unfold

依 MKO 的定義，f:X→Y 是函數，當且僅當 X 中每個輸入都在 Y 中有輸出（存在），而且只有一個（唯一）。對規則 x↦x²，存在性就是 x²∈Y；唯一性是：若 y、y′ 都等於 x²，則 y=y′。



S03 · implies操作前

(-2)^2,\ (-1)^2,\ 0^2,\ 1^2,\ 2^2

操作後

4,\ 1,\ 0,\ 1,\ 4

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + neg_mul

逐一計算 X 的五個輸入的平方：(−2)²=4、(−1)²=1、0²=0、1²=1、2²=4。負數的平方是正數，所以 −2 與 2 得到同一個值。



S04 · implies操作前

f(x)\in\{4,1,0,1,4\}

操作後

\forall x\in X:\ f(x)\in Y

條件：無

規則：finite_forall · 依賴：S03, G1

葉節點依據：finite_forall + numeric_evaluation

4、1、0 都在 Y={0,1,2,3,4,5} 的列舉中。X 是有限列舉，五個輸入全部檢查過，依 finite_forall，每個輸入都在 Y 中有輸出。這是對 X 全部元素的窮舉，不是抽樣；若 X 有無限多個元素，就需要一般論證。



S05 · implies操作前

y=x^2,\ y'=x^2

操作後

y=y'

條件：無

規則：eq_refl_symm_trans · 依賴：S02

葉節點依據：eq_refl_symm_trans + forall_intro

設對同一個 x，y 與 y′ 都是 f 的輸出，即 y=x²、y′=x²。依等號的對稱與傳遞，y=y′。x² 是由 x 確定的一個數，所以一個輸入不會有兩個不同輸出。這個論證對每個 x 都成立，不需逐一檢查。



S06 · implies操作前

\text{existence (S04)},\ \text{uniqueness (S05)}

操作後

f:X\to Y\ \text{is a function}

條件：無

規則：mko_function_def · 依賴：S02, S04, S05

葉節點依據：mko_function_def + and_intro_elim

存在性（S04）與唯一性（S05）都成立，依 S02 的等價，f:X→Y 是函數，滿足假設 a2。



S07 · equivalent操作前

f(X)=\{f(x)\mid x\in X\}

操作後

f(X)=\{0,1,4\}

條件：無

規則：image_preimage_def · 依賴：S03, S06

葉節點依據：image_preimage_def + finite_forall + set_extensionality

值域（像）是實際輸出的集合 f(X)={f(x) ∣ x∈X}。由 S03，輸出依次是 4、1、0、1、4；重複的輸出在集合中只算一次，所以 f(X)={0,1,4}。



S08 · implies操作前

f(X)=\{0,1,4\}\subseteq Y,\ 2\in Y

操作後

2\notin f(X),\ f(X)\neq Y

條件：無

規則：L_no_root_2 · 依賴：S04, S07

葉節點依據：quantifier_negation + finite_forall + set_extensionality + injective_surjective_def

f(X)⊆Y（每個輸出都在 Y 中，S04）。依引理 L_no_root_2（在 S08.1、S08.2 證明），X 中沒有 x 使 x²=2，所以 2∉f(X)；但 2∈Y。因此 f(X)≠Y：陪域不等於值域，f:X→Y 不是滿射。這正是 MKO 說的「陪域 Y 不必等於實際值域」。同理 3、5 也不在 f(X) 中。



S09 · equivalent操作前

\Gamma_f=\{(x,f(x))\mid x\in X\}

操作後

\Gamma_f=\{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}\subseteq X\times Y

條件：無

規則：graph_def · 依賴：S03, S06

葉節點依據：graph_def + cartesian_product_def + finite_counting_basics + numeric_evaluation

依圖形定義，代入 S03 的值得到五個有序對。Γ_f 是 X×Y 的子集合：X×Y 有 5·6=30 個有序對，Γ_f 只取其中 5 個，每個輸入恰好一個。比較三個對象：陪域 Y 有 6 個數，值域 f(X) 有 3 個數，圖形 Γ_f 有 5 個有序對。前兩者是 Y 的子集合，圖形是 X×Y 的子集合；它們是不同的數學對象。



S10 · implies操作前

f(-1)=1,\ f(1)=1

操作後

f(-1)=f(1),\ -1\neq 1:\ f\ \text{not injective}

條件：無

規則：injective_surjective_def · 依賴：S03

葉節點依據：injective_surjective_def + numeric_evaluation

f(−1)=1=f(1)，但 −1≠1，所以 f 不是單射：不同輸入可以有相同輸出。這不違反函數定義，因為定義只要求每個輸入的輸出唯一，不要求每個輸出只來自一個輸入。



S11 · implies操作前

f_1:X\to\{0,1,4\},\ f_1(x)=x^2

操作後

f_1\ \text{is a surjective function},\ f_1\neq f

條件：無

規則：function_def · 依賴：S03, S05, S08

葉節點依據：function_def + injective_surjective_def + set_extensionality

用同一規則宣告 f₁:X→{0,1,4}。S11.1 到 S11.3 證明：f₁ 是函數、是滿射，而且 f₁≠f。f₁ 與 f 有相同的規則、圖形與值域，只差在陪域；依 function_def，陪域是函數資料的一部分。



S12 · implies操作前

y=1:\ \{x\in X\mid x^2=1\}

操作後

\{-1,1\}:\ \text{two candidate outputs}

條件：無

規則：mko_function_def · 依賴：G3, S03

葉節點依據：mko_function_def + finite_forall + numeric_evaluation

考慮反向規則 s：對 y∈Y，s(y) 是 X 中滿足 x²=y 的 x。y=1 時，x=−1 與 x=1 都滿足（S03），而 −1≠1：一個輸入有兩個候選輸出，唯一性失敗，所以 s 不是 Y→X 的函數。這與 S10 的非單射直接相關。



S13 · implies操作前

y=2:\ \{x\in X\mid x^2=2\}

操作後

\varnothing:\ \text{no output}

條件：無

規則：mko_function_def · 依賴：G3, S08

葉節點依據：mko_function_def + quantifier_negation + finite_forall

y=2 時，依引理 L_no_root_2，X 中沒有 x 使 x²=2：這個輸入沒有輸出，存在性也失敗。S12 與 S13 各自就足以說明 s 不是 Y→X 的函數；s 同時犯了「多個輸出」與「沒有輸出」兩種錯。



S14 · implies操作前

g(2)=2+4

操作後

g(2)=6\notin Y:\ g\ \text{is not a function }X\to Y

條件：無

規則：mko_function_def · 依賴：G1, G3

葉節點依據：mko_function_def + numeric_evaluation

規則 g(x)=x+4 在輸入 2 給出 6，而 6∉Y（Y 的最大元素是 5），所以輸入 2 在 Y 中沒有輸出，g 不是 X→Y 的函數。同一規則若宣告為 g:X→ℤ，每個 x+4 都是唯一的整數，就是函數。是否為函數取決於宣告的陪域，不只取決於公式。



S15 · implies操作前

f,\ f_1,\ s,\ g

操作後

f,f_1\ \text{functions};\ f(X)=\{0,1,4\}\neq Y;\ s,g\ \text{not functions as declared}

條件：無

規則：and_intro_elim · 依賴：S06, S07, S08, S09, S11, S12, S13, S14

葉節點依據：and_intro_elim

彙整：f:X→Y 是函數（S06），值域 {0,1,4} 不等於陪域 Y（S07、S08），圖形是 5 個有序對（S09）；換陪域得到不同的滿射 f₁（S11）；s 不是 Y→X 的函數（S12、S13）；g 不是 X→Y 的函數（S14）。







## 局部子步與引理

S08.1 · equivalent操作前

\neg\exists x\in X:\ x^2=2

操作後

\forall x\in X:\ x^2\neq 2

條件：無

規則：quantifier_negation · 依賴：image_preimage_def

葉節點依據：quantifier_negation + image_preimage_def

2∈f(X) 依像的定義是 ∃x∈X, x²=2。依量詞否定，「沒有這樣的 x」等價於「每個 x∈X 都有 x²≠2」。



S08.2 · implies操作前

x^2\in\{4,1,0,1,4\}\ (x\in X)

操作後

\forall x\in X:\ x^2\neq 2

條件：無

規則：finite_forall · 依賴：S03, S08.1

葉節點依據：finite_forall + numeric_evaluation

由 S03，X 的五個輸入的平方是 4、1、0、1、4，沒有一個等於 2。依 finite_forall，∀x∈X, x²≠2；再依 S08.1，X 中沒有 x 使 x²=2。S08.1 與 S08.2 合起來證得引理 L_no_root_2。



S11.1 · implies操作前

f_1(x)\in\{4,1,0,1,4\}

操作後

f_1:X\to\{0,1,4\}\ \text{is a function}

條件：無

規則：finite_forall · 依賴：S03, S05

葉節點依據：finite_forall + mko_function_def

由 S03，五個輸出都在 {0,1,4} 中，依 finite_forall 存在性成立；唯一性與 S05 相同。所以 f₁ 是函數。



S11.2 · implies操作前

0=f_1(0),\ 1=f_1(1),\ 4=f_1(2)

操作後

f_1\ \text{is surjective}

條件：無

規則：injective_surjective_def · 依賴：S03, S11.1

葉節點依據：injective_surjective_def + finite_forall + exists_intro

陪域 {0,1,4} 的每個元素都有原像：0=f₁(0)、1=f₁(1)、4=f₁(2)。依 finite_forall 與滿射定義，f₁ 是滿射。



S11.3 · implies操作前

\text{codomain of }f_1=\{0,1,4\},\ \text{codomain of }f=Y

操作後

f_1\neq f

條件：無

規則：function_def · 依賴：S08, S11.1

葉節點依據：function_def + set_extensionality

2∈Y 但 2∉{0,1,4}，所以兩個陪域不同。依 function_def，兩函數相等需要相同的定義域、陪域與每點的值，所以 f₁≠f，儘管兩者每點的值都相同。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S06, S07, S08, S09, S11, S12, S13, S14, and_intro_elim — 目標 G 是題目各項結論的合取；每一項都由所列步驟正向證成，此步只做合取，沒有把 G 當作前提。
- S14 · premise_audit · mko_function_def, G1, numeric_evaluation — 一個輸出落在陪域外就足以否定 g:X→Y；對 g:X→ℤ 的肯定只用到整數對加法封閉。
- S13 · premise_audit · L_no_root_2, mko_function_def — 只需一個沒有輸出的輸入；結論依賴 X 的具體內容。
- S12 · premise_audit · mko_function_def, S03 — 一個違反唯一性的輸入就足以否定是函數。
- S11.3 · premise_audit · function_def, set_extensionality — 依賴「陪域是函數資料的一部分」這個約定（function_def，與 MKO 一致）；若只把函數看作圖形，f 與 f₁ 會被視為相同，本稿不採這個約定。
- S11.2 · premise_audit · injective_surjective_def, finite_forall — 陪域三個元素逐一給出原像，是完整檢查。
- S11.1 · premise_audit · S03, S05, finite_forall, mko_function_def — 需要每個輸出都落在新陪域中；這是對 X 的完整檢查。
- S11 · premise_audit · function_def, injective_surjective_def — 三個子結論各由一個子步給出；不宣稱 f₁ 是單射（f₁(−1)=f₁(1)）。
- S10 · premise_audit · injective_surjective_def, S03 — 一組反例就足以否定單射；不宣稱這影響 f 是否為函數（S06 已證 f 是函數）。
- S09 · inverse_equivalence · graph_def, finite_forall, set_extensionality — 對 X 的每個元素各有一對，列舉與定義元素相同，雙向成立。
- S08.2 · premise_audit · S03, finite_forall — 五個元素全部檢查，所以對 X 是完整的；N6 以 x=−2 到 2 的整數重做同一檢查，那正是 X 的全部元素。
- S08.1 · inverse_equivalence · quantifier_negation — 量詞否定本身是等價，雙向成立。
- S08 · premise_audit · L_no_root_2, set_extensionality, injective_surjective_def — 一個屬於 Y 而不屬於 f(X) 的元素就足以否定 f(X)=Y。2∉f(X) 依賴對 X 全部輸入的檢查（引理）；在 ℝ 中 x²=2 有解 √2，所以結論只對這個 X 成立。
- S07 · inverse_equivalence · image_preimage_def, set_extensionality, finite_forall — y∈f(X) ⇔ 有某個 x∈X 使 f(x)=y；依 finite_forall 逐一對照五個輸入，兩邊元素相同，雙向成立。
- S06 · sufficient_goal_reduction · S02, S04, S05, mko_function_def — 目標 G：f 是 X→Y 的函數。足夠條件 H：存在性與唯一性；H⇒G 由 S02。H 由 S04、S05 正向證成，沒有把 G 當作前提。
- S05 · premise_audit · eq_refl_symm_trans, forall_intro — 只用到等號的性質；反向「不同輸入有不同輸出」並未宣稱，S10 證明它不成立。
- S04 · premise_audit · S03, finite_forall — 窮舉之所以足夠，是因為 X 恰好是這五個元素（G1）；反向（Y 的每個元素都是輸出）並未宣稱，S08 證明它不成立。
- S03 · premise_audit · numeric_evaluation, G1 — 每個值都可獨立重算（N1 到 N5）；X 恰好有這五個元素，所以這是完整計算。
- S02 · inverse_equivalence · mko_function_def, function_def — 這是定義的展開，雙向成立；三個要求（有輸出、輸出在 Y 中、輸出唯一）缺一不可。
- S01 · premise_audit · G1, G2, def_intro — 此步只宣告；f 是否真的是 X→Y 的函數（假設 a2）要在 S02 到 S06 檢查，不能預設。





## 錯誤控制與反例

陪域、值域、圖形是三個不同對象MKO 指出常見誤解是把陪域、值域與函數圖形視為同一個對象。本例：陪域 Y={0,1,2,3,4,5} 是宣告的一部分；值域 f(X)={0,1,4} 是實際輸出；圖形 Γ_f 是由 X×Y 中 5 個有序對組成的子集合（S07 到 S09）。改變陪域會改變函數（S11），卻不改變值域與圖形。

程式函數不等於數學總函數MKO 也提醒不要把有副作用或失敗狀態的程式函數等同於純數學總函數。例如一段程式依次搜尋 −2、−1、0、1、2，傳回第一個平方等於 y 的數：y=1 時它傳回 −1（搜尋次序代替了唯一性），y=2 時它找不到而失敗。這段程式「能執行」，但它並沒有把 s 變成 Y→X 的函數（S12、S13）；它是另一個加了選擇規則、而且在 y=2 等處沒有定義的對象。

唯一性是對輸入而言最容易做錯的是把兩個條件混淆：函數要求每個輸入只有一個輸出（S05），並不要求每個輸出只來自一個輸入。f(−1)=f(1) 不影響 f 是函數（S10）；反過來，s 在 y=1 有兩個輸出才違反定義（S12）。


- f 的陪域是 {0,1,4} → reject — 宣告的陪域是 Y={0,1,2,3,4,5}；{0,1,4} 是值域（S07、S08）。
- f(−1)=f(1)，所以 f 不是函數 → reject — 函數只要求每個輸入的輸出唯一；f 只是不是單射（S06、S10）。
- s(y)=「X 中滿足 x²=y 的 x」定義了 Y→X 的函數 → reject — y=1 有兩個候選 −1、1，y=2 沒有候選（S12、S13）。
- g(x)=x+4 是 X→Y 的函數 → reject — g(2)=6∉Y（S14）。
- f 與 f₁ 有相同的圖形，所以 f=f₁ → reject — 陪域不同（2∈Y 但 2∉{0,1,4}），依 function_def 兩者不同（S11.3）。





## 結論與限制

f:X→Y，f(x)=x²，是函數：每個輸入在 Y 中恰有一個輸出。它的值域是 {0,1,4}，不等於陪域 Y={0,1,2,3,4,5}（2∉f(X)），圖形是 {(−2,4),(−1,1),(0,0),(1,1),(2,4)}；陪域、值域、圖形是三個不同的對象。把陪域改為 {0,1,4} 得到不同的函數 f₁，它是滿射。反向規則 s 在 y=1 有兩個候選、在 y=2 沒有輸出，不是函數；g(x)=x+4 因 g(2)=6∉Y 而不是 X→Y 的函數。


- N6 在 x=−2 到 2 的整數上核對 x²≠2；這五個整數恰好是 X 的全部元素，所以對 X 是完整檢查，但它不說明 x²=2 在其他集合（例如 ℝ，有解 √2）中無解。
- 本稿採用「陪域是函數資料的一部分」的約定（function_def，與 MKO 一致）；以圖形定義函數的教材會得到不同的 f=f₁ 判斷。





## 驗證及來源綁定

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


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

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