# 函數映射

符號 f:X→Y 表示函數 f 從定義域 X 映射到陪域 Y。

mko-function-mapping · definition · v0.8.0



## 數學敘述

函數 f:X→Y 對 X 中每一個輸入指定 Y 中唯一一個輸出；陪域 Y 不必等於實際值域。





## 代表公式（精確 TeX）

f:X\to Y





## 成立條件


- X 與 Y 是已指定的集合或相容類型。
- X 中每個輸入在 f 下都有且只有一個輸出。





## 符號作用域


- f — 函數
- X — 定義域
- Y — 陪域
- → — 映射箭頭





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

函數的核心不是一條畫出來的曲線，而是每個允許輸入都對應唯一輸出的規則。

f:X→Y 宣告了定義域與陪域；實際輸出形成的值域可能只是 Y 的一部分。

Lean 定理 function_total_unique 已對任意 f:X→Y 與 x:X 證明存在唯一 y:Y 使 f x=y。

把陪域、值域與函數圖形視為同一個數學對象，或把具有副作用與失敗狀態的程式函數直接等同於純數學總函數。





## 已採用的推導導讀

[函數映射：判定對應是否為函數，並分辨陪域、值域與圖形](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-function-mapping-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合隸屬](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-membership/) — 函數輸入與輸出分別屬於定義域與陪域。





## 驗證界線

Lean 已形式化總函數對每個輸入存在唯一輸出的核心語義；部分函數、副作用、隨機性與執行失敗不在此聲明內。

formalized_total_function_core


- [evidence-sha256-d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b](https://ocme.evemisslab.com/data/evidence/d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b.json)





## 下一個義務

新增值域、單射、滿射、雙射與部分函數物件，明確區分型別陪域與實際輸出集合。





## 同源結構化資料

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

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