# 實值函數圖形

固定直角座標系後，實值函數的圖形是全部合法輸入與其唯一輸出組成的有序對集合。

mko-function-graph · definition · v0.10.0



## 數學敘述

對 D⊆R 及總函數 f:D→R，在固定平面直角座標系中定義 G_f={(x,f(x)):x∈D}。有序對 (u,v) 屬於 G_f，當且僅當 u∈D 且 v=f(u)。





## 代表公式（精確 TeX）

P(x,f(x))





## 成立條件


- 座標系固定、兩座標為有序實數對；先宣告定義域 D。
- f 在每個 D 中輸入恰有一個實數輸出；有限表格若宣告陪域 B，所有輸出還须落在 B。





## 符號作用域


- P — 圖形上的點記號
- x — 定義域輸入
- f — 實值總函數





## 直觀、定義與常見誤解

成員判定同時檢查 u∈D 和等式 v=f(u)。即使某個公式在域外也可求值，該點仍不在宣告的函數圖形內。

有限圖形可依第一座標排序，重複有序對只列一次。給定 D 和 B 時，要逐輸入檢查恰有一個 B 中的輸出，也不能多出 D 外的圖形點；這是指定總函數的表格驗證。

垂直線測試檢查每個輸入至多一個輸出，單独不足以檢查對宣告 D 的總定義性。示意圖不提供精確座標；圖形的單點或有限資料也不自動建立反函數、滿射或全域公式。

只檢查 y=f(x) 而漏掉定義域，或把垂直線至多一點誤當宣告域上每點恰有輸出。





## 已採用的推導導讀

[實值函數圖形：成員判定與有限表格的總函數驗證](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-function-graph-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 每個合法輸入須有唯一輸出。
- [座標平面](https://ocme.evemisslab.com/zh-Hant/mko/mko-coordinate-plane/) — 函數圖形的兩座標依固定座標系解讀。





## 驗證界線

本輪有限明示圖形和整數仿射輸入可精確驗證；一般圖形集合與幾何表示橋仍待形式化。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定 Set.graph、實數乘積座標表示、域限制及有限總函數表格語義。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/function-graph.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-graph/index.md)