# 實值函數圖形：成員判定與有限表格的總函數驗證

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

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

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



## 目標與範圍

(一) 設 D=[0,2]、f:D→ℝ、f(x)=x²−1。先證明 (u,v)∈G_f ⇔ u∈D 且 v=f(u)，再判定 (1,0)、(−1,0)、(2,2)、(2,3) 是否在 G_f 上。(二) 設 D_0={0,1,2}、B={0,1,4}。證明一個集合 Γ 是某個總函數 D_0→B 的圖形，當且僅當 Γ⊆D_0×B 且每個輸入恰有一個輸出；據此判定 T={(0,0),(1,1),(2,4)} 是、而 T_1={(0,0),(2,4)}、T_2={(0,0),(1,1),(1,4),(2,4)}、T_3={(0,0),(1,1),(2,4),(3,9)} 都不是。

在 MKO 的範圍內：固定直角座標系、實數有序對，先宣告定義域；總函數在每個輸入恰有一個輸出，有限表格另需輸出落在宣告的陪域 B。不從示意圖讀坐標，不從有限資料推出反函數、滿射或全域公式；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- function_def
- set_builder
- set_extensionality
- order_basics
- numeric_evaluation


- G1 — 固定平面直角座標系，點以實數有序對表示；先宣告定義域，總函數在定義域的每個輸入恰有一個實數輸出（MKO 假設 a1、a2）。
- G2 — D=[0,2]={x∈ℝ ∣ 0≤x≤2}，f:D→ℝ，f(x)=x²−1；待判定的有序對為 (1,0)、(−1,0)、(2,2)、(2,3)。
- G3 — D_0={0,1,2}，B={0,1,4}；候選表格 T={(0,0),(1,1),(2,4)}、T_1={(0,0),(2,4)}、T_2={(0,0),(1,1),(1,4),(2,4)}、T_3={(0,0),(1,1),(2,4),(3,9)}。


- D,\ D_0 — 宣告的定義域：D=[0,2]，D_0={0,1,2}
- B — 有限表格宣告的陪域 {0,1,4}
- G_f=\{(x,f(x))\mid x\in D\} — f 的圖形
- T,\ T_1,\ T_2,\ T_3 — 四個候選表格（有序對的有限集合）
- \Gamma — 一般的候選有序對集合





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- 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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- 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)。
- mko_graph_def · cited — 對 D⊆R 及總函數 f:D→R，在固定平面直角座標系中定義 G_f={(x,f(x)):x∈D}。有序對 (u,v) 屬於 G_f，當且僅當 u∈D 且 v=f(u)。 · mko-function-graph
- mko_table_check · cited — 有限圖形可依第一座標排序，重複有序對只列一次。給定 D 和 B 時，要逐輸入檢查恰有一個 B 中的輸出，也不能多出 D 外的圖形點；這是指定總函數的表格驗證。 · mko-function-graph
- L_graph_member · lemma — 對任何總函數 f:D→ℝ 與實數 u、v：(u,v)∈G_f ⇔ u∈D 且 v=f(u)。
- L_table_graph · lemma — 對集合 D、B⊆ℝ 與 Γ⊆ℝ²：Γ 是某個總函數 F:D→B 的圖形，當且僅當 Γ⊆D×B 且每個 u∈D 恰有一個 v 使 (u,v)∈Γ。





## 逐步主鏈

S01 · definition操作前

f:D\to\mathbb{R}\ \text{total},\ D\subseteq\mathbb{R}

操作後

G_f=\{(x,f(x))\mid x\in D\}\subseteq\mathbb{R}^2

條件：D\ \text{declared}

規則：mko_graph_def · 依賴：G1, G2

葉節點依據：mko_graph_def + set_builder

依 MKO，圖形是讓 x 走遍宣告的定義域 D 時得到的有序對 (x,f(x)) 的集合。定義域是圖形定義的一部分：同一個公式配上不同的 D，就是不同的函數、不同的圖形。



S02 · equivalent操作前

(u,v)\in G_f

操作後

u\in D\ \land\ v=f(u)

條件：無

規則：L_graph_member · 依賴：S01

葉節點依據：set_builder + cartesian_product_def + exists_intro + exists_elim

依引理 L_graph_member，成員判定要同時檢查兩件事：u 在定義域中，且 v 等於 f(u)。兩個方向在 S02.1、S02.2 證明。



S03 · implies操作前

(1,0)

操作後

1\in D,\ f(1)=1^2-1=0\ \Rightarrow\ (1,0)\in G_f

條件：0\le 1\le 2

規則：L_graph_member · 依賴：S02, G2

葉節點依據：L_graph_member + order_basics + numeric_evaluation

第一個條件：0≤1≤2，所以 1∈D。第二個條件：f(1)=1²−1=0，等於第二坐標 0。兩者都成立，依 S02，(1,0)∈G_f。



S04 · implies操作前

(-1,0)

操作後

-1\notin D\ \Rightarrow\ (-1,0)\notin G_f

條件：-1<0

規則：L_graph_member · 依賴：S02, G2

葉節點依據：L_graph_member + order_basics + numeric_evaluation

公式在 x=−1 也能求值：(−1)²−1=0，與第二坐標相等。但 −1<0，所以 −1∉D=[0,2]，S02 的第一個條件不成立，(−1,0)∉G_f。這正是 MKO 提醒的情形：公式在域外可求值，不代表該點在宣告的圖形內。



S05 · implies操作前

(2,2),\ (2,3)

操作後

f(2)=3:\ (2,2)\notin G_f,\ (2,3)\in G_f

條件：0\le 2\le 2

規則：L_graph_member · 依賴：S02, G2

葉節點依據：L_graph_member + function_def + numeric_evaluation

0≤2≤2，所以 2∈D（端點包含在閉區間內）。f(2)=2²−1=3。(2,2) 的第二坐標 2≠3，所以 (2,2)∉G_f；(2,3) 兩個條件都成立，(2,3)∈G_f。G_f 中第一坐標為 2 的點恰有 (2,3) 一個，因為 f 在 2 只有一個輸出。



S06 · equivalent操作前

\Gamma\ \text{is the graph of some total}\ F:D\to B

操作後

\Gamma\subseteq D\times B\ \land\ \forall u\in D\ \exists!\,v:\ (u,v)\in\Gamma

條件：無

規則：L_table_graph · 依賴：G3, S02

葉節點依據：function_def + set_extensionality + L_graph_member

依引理 L_table_graph，有限表格是不是一個總函數 D→B 的圖形，可用兩個條件判定：不多出 D×B 之外的點，且每個輸入恰有一個輸出。這是 MKO para1 的表格驗證；兩個方向在 S06.1、S06.2 證明。



S07 · implies操作前

T=\{(0,0),(1,1),(2,4)\}

操作後

T\subseteq D_0\times B

條件：無

規則：cartesian_product_def · 依賴：G3, cartesian_product_def

葉節點依據：cartesian_product_def + subset_def

逐一檢查 T 的三個有序對：第一坐標 0、1、2 都在 D_0={0,1,2} 中，第二坐標 0、1、4 都在 B={0,1,4} 中。所以每個元素都屬於 D_0×B。



S08 · case_split操作前

u\in D_0=\{0,1,2\}

操作後

u=0\mapsto 0,\ u=1\mapsto 1,\ u=2\mapsto 4,\ \text{each exactly once}

條件：無

規則：case_analysis · 依賴：G3, S07

葉節點依據：case_analysis + and_intro_elim

D_0 只有三個元素，逐一檢查：第一坐標為 0 的有序對只有 (0,0)，為 1 的只有 (1,1)，為 2 的只有 (2,4)。每個輸入恰有一個輸出：既不缺（存在），也不多（唯一）。



S09 · theorem_application操作前

T\subseteq D_0\times B,\ \forall u\in D_0\ \exists!\,v

操作後

T=G_F,\ F:D_0\to B,\ F(0)=0,\ F(1)=1,\ F(2)=4

條件：無

規則：L_table_graph · 依賴：S06, S07, S08

葉節點依據：L_table_graph + function_def

S07 與 S08 正是 L_table_graph 的兩個條件，依 ⇐ 方向（S06.1），T 是總函數 F:D_0→B 的圖形，F(0)=0、F(1)=1、F(2)=4。這三個值恰與 x² 在 0、1、2 的值相同，但本稿不宣稱 F 在 D_0 之外有任何公式。



S10 · implies操作前

T_1=\{(0,0),(2,4)\}

操作後

\neg\exists v:(1,v)\in T_1\ \Rightarrow\ T_1\ \text{is not the graph of a total}\ D_0\to B

條件：1\in D_0

規則：contrapositive · 依賴：S06, G3

葉節點依據：contrapositive + L_table_graph + quantifier_negation

T_1 中每個第一坐標至多出現一次（0 對應 0、2 對應 4），所以它通過垂直線測試。但 1∈D_0，而 T_1 中沒有第一坐標為 1 的有序對，存在性失敗。依 S06.2 的逆否，T_1 不是任何總函數 D_0→B 的圖形。垂直線測試只檢查「至多一個」，不檢查宣告域上的「至少一個」。



S11 · implies操作前

T_2=\{(0,0),(1,1),(1,4),(2,4)\}

操作後

(1,1),(1,4)\in T_2,\ 1\neq 4\ \Rightarrow\ T_2\ \text{is not a function graph}

條件：無

規則：contrapositive · 依賴：S06, G3

葉節點依據：contrapositive + L_table_graph + numeric_evaluation

輸入 1 在 T_2 中有兩個不同的輸出 1 與 4，唯一性失敗（垂直線 x=1 與 T_2 交於兩點）。依 S06.2 的逆否，T_2 不是任何總函數 D_0→B 的圖形；雖然它的四個點都在 D_0×B 中。



S12 · implies操作前

T_3=\{(0,0),(1,1),(2,4),(3,9)\}

操作後

(3,9)\notin D_0\times B\ \Rightarrow\ T_3\ \text{is not the graph of a total}\ D_0\to B

條件：3\notin D_0

規則：contrapositive · 依賴：S06, G3

葉節點依據：contrapositive + L_table_graph + cartesian_product_def

T_3 在 D_0 的每個輸入恰有一個輸出，但多了一點 (3,9)：3∉D_0（而且 9∉B），所以 T_3⊄D_0×B。依 S06.2 的逆否，T_3 不是總函數 D_0→B 的圖形。MKO 要求表格不能多出 D 外的圖形點。



S13 · implies操作前

\text{four pairs and four tables}

操作後

(1,0),(2,3)\in G_f;\ (-1,0),(2,2)\notin G_f;\ T\ \text{accepted};\ T_1,T_2,T_3\ \text{rejected}

條件：無

規則：and_intro_elim · 依賴：S03, S04, S05, S09, S10, S11, S12

葉節點依據：and_intro_elim

彙整：(1,0) 與 (2,3) 在 G_f 上；(−1,0) 因 −1∉D、(2,2) 因 2≠f(2) 而不在。T 是總函數 D_0→B 的圖形；T_1 缺輸出、T_2 輸出不唯一、T_3 有域外點，都不是。







## 局部子步與引理

S02.1 · implies操作前

(u,v)\in G_f

操作後

u\in D\ \land\ v=f(u)

條件：無

規則：cartesian_product_def · 依賴：S01, cartesian_product_def

葉節點依據：exists_elim + cartesian_product_def + eq_replace

(u,v)∈G_f 表示有某個 x∈D 使 (u,v)=(x,f(x))。依有序對相等條件，u=x 且 v=f(x)。把 x 換成 u：u∈D，且 v=f(u)。這是 ⇒ 方向。



S02.2 · implies操作前

u\in D\ \land\ v=f(u)

操作後

(u,v)=(u,f(u))\in G_f

條件：無

規則：exists_intro · 依賴：S01, exists_intro

葉節點依據：exists_intro + cartesian_product_def

若 u∈D 且 v=f(u)，則 (u,v)=(u,f(u))，取 x=u∈D 作見證，(u,v) 屬於 G_f。這是 ⇐ 方向。S02.1 與 S02.2 合起來證得引理 L_graph_member。



S06.1 · implies操作前

\Gamma\subseteq D\times B,\ \forall u\in D\ \exists!\,v:(u,v)\in\Gamma

操作後

F(u):=\text{the unique}\ v,\quad F:D\to B\ \text{total},\quad G_F=\Gamma

條件：無

規則：function_def · 依賴：S02, function_def, set_extensionality

葉節點依據：function_def + set_extensionality + L_graph_member

⇐ 方向：對每個 u∈D，令 F(u) 為那個唯一的 v；因 Γ⊆D×B，F(u)∈B，所以 F:D→B 是總函數。再證 G_F=Γ：由 L_graph_member，(u,v)∈G_F ⇔ u∈D 且 v=F(u)。若 u∈D 且 v=F(u)，依 F 的取法 (u,v)∈Γ；反之若 (u,v)∈Γ，則 u∈D（Γ⊆D×B），且依唯一性 v=F(u)。依 set_extensionality，G_F=Γ。



S06.2 · implies操作前

\Gamma=G_F,\ F:D\to B\ \text{total}

操作後

\Gamma\subseteq D\times B\ \land\ \forall u\in D\ \exists!\,v:(u,v)\in\Gamma

條件：無

規則：L_graph_member · 依賴：S02, function_def

葉節點依據：L_graph_member + function_def + subset_def

⇒ 方向：若 Γ=G_F，Γ 的每個元素都是 (x,F(x))，x∈D、F(x)∈B，所以 Γ⊆D×B。對 u∈D，依 L_graph_member，(u,v)∈Γ ⇔ v=F(u)，所以恰有一個 v，即 F(u)。S06.1 與 S06.2 合起來證得引理 L_table_graph。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S03, S04, S05, S09, S10, S11, S12, and_intro_elim — 目標 G：八個判定。足夠條件 H：S03 至 S12 的各別結論；H⇒G 只是合取。H 由定義與兩個引理正向證成，沒有把 G 當作前提。
- S12 · premise_audit · S06, contrapositive, cartesian_product_def — 「每個輸入恰有一個輸出」只是條件之一；Γ⊆D×B 也必須成立。
- S11 · premise_audit · S06, contrapositive — 1≠4（N9）即足以推翻唯一性；不需要檢查其他輸入。
- S10 · premise_audit · S06, contrapositive, G3 — 結論只針對宣告的 D_0；T_1 是定義在 {0,2} 上的函數圖形，但那是另一個定義域。
- S09 · premise_audit · S06, S07, S08, L_table_graph — 兩個條件都已正向證成；三點與 x² 吻合（N8、N11、N12）只是觀察，不是全域公式的證據。
- S08 · premise_audit · case_analysis, G3 — 三個情形涵蓋 D_0 的全部元素；存在與唯一兩項都要檢查。
- S07 · premise_audit · cartesian_product_def, subset_def — 有限集合可逐一列舉檢查，這是完整的檢查而非抽樣。
- S06.2 · premise_audit · S02, function_def — 這個方向的逆否是拒絕表格的依據：只要缺一個輸出、多一個輸出或多出域外點，就不是總函數 D→B 的圖形。
- S06.1 · premise_audit · function_def, set_extensionality, S02 — 存在性給出 F 在每點有定義（總），唯一性給出 F 是函數且 Γ⊆G_F；Γ⊆D×B 保證輸出落在 B 且沒有域外點。
- S06 · inverse_equivalence · L_table_graph, mko_table_check — 引理兩個方向都在子步證明，所以可作為等價使用；後面用 ⇐ 接受 T，用 ⇒ 的逆否拒絕 T_1、T_2、T_3。
- S05 · premise_audit · S02, numeric_evaluation, function_def — u∈D 不夠，v=f(u) 也必須成立（N6、N7）。
- S04 · premise_audit · S02, order_basics, numeric_evaluation — 只要一個條件不成立就推出不屬於（N4、N5）；不需要也不應只看等式。
- S03 · premise_audit · S02, numeric_evaluation, order_basics — 兩個條件都核對了（N1、N2、N3），缺一不可。
- S02.2 · premise_audit · exists_intro, cartesian_product_def — 見證 x=u 必須在 D 中；若 u∉D，即使 v 等於公式的值，也找不到見證。
- S02.1 · premise_audit · cartesian_product_def, exists_elim, eq_replace — 取出見證 x 後，結論不含 x，符合 ∃消去的規則。
- S02 · inverse_equivalence · L_graph_member — 引理兩個方向都已在子步證明，所以可作為等價使用。
- S01 · premise_audit · G1, G2, mko_graph_def — 此步只寫出定義；用到 f 是總函數，所以每個 x∈D 都貢獻恰好一點。





## 錯誤控制與反例

只檢查 y=f(x) 會漏掉定義域MKO 指出的第一個誤解是只檢查等式而漏掉定義域。(−1,0) 滿足 0=(−1)²−1，但 −1∉[0,2]，所以不在 G_f 上（S04）。成員判定必須同時檢查 u∈D 與 v=f(u)（S02）。

垂直線測試不等於總定義MKO 指出的第二個誤解是把「垂直線至多交一點」當成「宣告域上每點恰有輸出」。T_1 每條垂直線至多交一點，但輸入 1 沒有輸出，所以不是總函數 D_0→B 的圖形（S10）。完整的表格驗證還要檢查沒有域外點（S12）。

有限表格不決定域外延伸，示意圖不替代精確資料T 在 0、1、2 的值與 x² 相同，但這不推出 F 在其他地方的公式，F 甚至只定義在 D_0 上（S09）。示意圖不提供精確坐標；有限資料也不自動建立反函數或滿射（MKO para2）。


- (−1,0)∈G_f，因為 (−1)²−1=0 → reject — −1∉D=[0,2]；成員判定還要求第一坐標在定義域中。
- (2,2)∈G_f，因為 2∈D → reject — f(2)=3≠2；第二坐標必須等於 f(2)。
- T_1={(0,0),(2,4)} 通過垂直線測試，所以是總函數 D_0→B 的圖形 → reject — 1∈D_0 沒有輸出；垂直線測試不檢查總定義性。
- T_3 在 D_0 的每個輸入都恰有一個輸出，所以是總函數 D_0→B 的圖形 → reject — T_3 含 (3,9)，3∉D_0、9∉B，所以 T_3⊄D_0×B。
- T 與 x² 在 0、1、2 吻合，所以 F 就是 ℝ 上的函數 x² → reject — F 只定義在 D_0 上；有限資料不決定定義域外的值或全域公式。





## 結論與限制

(u,v)∈G_f 當且僅當 u∈D 且 v=f(u)。對 D=[0,2]、f(x)=x²−1：(1,0)、(2,3) 在圖形上；(−1,0) 不在（−1∉D，雖然公式值為 0）；(2,2) 不在（f(2)=3）。一個集合是總函數 D_0→B 的圖形，當且僅當它是 D_0×B 的子集合且每個輸入恰有一個輸出：T={(0,0),(1,1),(2,4)} 是；T_1 缺輸入 1 的輸出（雖通過垂直線測試）、T_2 在 1 有兩個輸出、T_3 多出 (3,9)，都不是。


- 本稿不討論圖形的幾何性質（連續、形狀），也不從圖形推出反函數或滿射。
- N8、N11、N12 只記錄 x² 在 0、2、1 的值為 0、4、1，與 T 在這三點的輸出相同；它們不支持任何全域公式。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: fd7c2071f9e6afa63b288de5141c6fb96961f0e1fe8adfbf5194e5cf438c7930
- original source SHA-256: 0b42b0a6e4a678932e19deb35bc9d4abbca16e6381f1a4c619ddbdb34f21a2b6
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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