# 定義域、陪域與值域

總函數 f:A→B 的定義域是 A，陪域是 B，值域是實際取得的輸出集合 f[A]。

mko-domain-codomain-range · definition · v0.10.0



## 數學敘述

對總函數 f:A→B，A 是允許的全部輸入，B 是宣告的輸出集合；值域 f[A]={f(x):x∈A} 是 B 的子集合，未必等於 B。





## 代表公式（精確 TeX）

f:A\to B





## 成立條件


- A、B 已明示，f 為在 A 上每個輸入恰有一個 B 中輸出的總函數。





## 符號作用域


- f — 總函數
- A — 定義域
- B — 陪域





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

定義域指定哪些輸入允許；陪域指定輸出必須落在哪裡。值域只收集實際出現的輸出，重複輸出只列一次。

同一份映射資料可以具有不同的合法陪域，但宣告 f:A→B 的完整函數資料因此不同。不可只看輸出表猜陪域。

有限表格可逐輸入驗證總函數，再分別讀出 A、B 與值域。漏掉輸入、多重輸出或輸出落在 B 外的表格，不能冒充本條目的總函數。

把陪域誤當實際值域，或以未定義輸入的表格計算一個宣称的總函數值域。





## 已採用的推導導讀

[定義域、陪域與值域：有限表格與 h(x)=x²+1 的值域](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-domain-codomain-range-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 三個集合角色依總函數的输入輸出條件定義。
- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 定義域、陪域與值域都是明示集合。





## 驗證界線

有限明示表格可完整檢查其輸入輸出；這不替代一般函數與无限集合的形式證明。

not_formalized

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





## 下一個義務

綁定 Set.range、像集合與函數型別的定義域／陪域橋。





## 同源結構化資料

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

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