# 滿射與陪域覆蓋

滿射要求陪域每個元素都有合法原像；相同輸出可以有多個原像。

mko-surjective · definition · v0.10.0



## 數學敘述

總函數 f:A→B 是滿射，當且僅當對每個 b∈B 都存在 x∈A 使 f(x)=b，也就是實際值域 f[A] 等於宣告陪域 B。滿射不要求原像唯一。





## 代表公式（精確 TeX）

f:A\to B





## 成立條件


- 定義域、陪域及總函數已明示。
- 更換陪域時仍須包含全部既有輸出，才能保持同一份表為合法總函數。





## 符號作用域


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





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

有限表的未覆蓋目標是 B∖f[A]。缺任一目標即不是滿射；多個輸入映到同一目標不會因此破壞滿射。

對指定 t∈B 可列出原像；首個原像僅指有限整數資料中按數值最小的原像，無原像時答不存在。

同一輸出表若把陪域從 B 改為 B2，滿射性可能改變。先確認 f[A]⊆B2，再問是否等於 B2，不能猜陪域或丟掉仍出現的輸出。空函數 ∅→∅ 為滿射，∅→非空 B 則不是。

把值域自動當成陪域，或以多個原像否定滿射。





## 已採用的推導導讀

[滿射與陪域覆蓋：值域、原像與陪域變更](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-surjective-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 陪域和輸出資格是函數宣告的一部分。
- [量詞與明示論域](https://ocme.evemisslab.com/zh-Hant/mko/mko-quantifier/) — 滿射是對每個陪域元素存在合法原像。





## 驗證界線

有限陪域覆蓋可完整重算；一般滿射與選擇原像的形式義務仍保留。

not_formalized

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





## 下一個義務

綁定 Function.Surjective、range 與陪域變更的合法性。





## 同源結構化資料

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

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