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

目標與範圍

(一) 設 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)∈Γ。

逐步主鏈

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

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

(u,v)\in G_f

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

(1,0)

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

(-1,0)

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

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

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

\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

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

T\subseteq D_0\times B

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

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

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

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

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}

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

\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}

局部子步與引理

(u,v)\in G_f

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

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

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

\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

\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

逐步反向審查

• 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、反控制與修訂記錄）