實值函數圖形

數學敘述

對 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) 而漏掉定義域，或把垂直線至多一點誤當宣告域上每點恰有輸出。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 函數映射 — 每個合法輸入須有唯一輸出。
• 座標平面 — 函數圖形的兩座標依固定座標系解讀。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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