滿射與陪域覆蓋

數學敘述

總函數 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 則不是。

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

已採用的推導導讀

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

前置知識

• 函數映射 — 陪域和輸出資格是函數宣告的一部分。
• 量詞與明示論域 — 滿射是對每個陪域元素存在合法原像。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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