# 雙射與唯一原像

雙射同時單射與滿射，等價於陪域每個元素恰有一個合法原像。

mko-bijective · definition · v0.10.0



## 數學敘述

總函數 f:A→B 為雙射，當且僅當它同時單射與滿射；等價地，每個 b∈B 的纖維恰有一個元素。對有限集合，存在某個 A→B 的雙射當且僅當 |A|=|B|；基數相等不保證任意給定 f 都是雙射。





## 代表公式（精確 TeX）

f:A\to B





## 成立條件


- 給定函數性質與是否存在某個雙射是不同問題。
- 基數存在性題限定有限集合，大小是非負整數；零到零包含唯一空雙射。





## 符號作用域


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





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

有限函數可分為雙射、僅單射、僅滿射、兩者皆非。不能只檢查兩個集合大小而忽略實際映射資料。

完整纖維概況按陪域目標排序，包含沒有原像的零纖維；全部纖維大小都為一才是雙射。

有限集合相同基數允許逐一配對形成某個雙射，但可能另有非雙射的函數。基數題只問存在可能性，不把它冒充給定函數的審定。

由 |A|=|B| 直接判給定 f 雙射，或只查其中一個條件。





## 已採用的推導導讀

[雙射：以纖維概況判定給定函數，並與「是否存在某個雙射」分開](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-bijective-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [單射與不同輸入的辨識](https://ocme.evemisslab.com/zh-Hant/mko/mko-injective/) — 雙射包含單射要求。
- [滿射與陪域覆蓋](https://ocme.evemisslab.com/zh-Hant/mko/mko-surjective/) — 雙射包含滿射要求。





## 驗證界線

有限纖維與基數切片可重算；一般雙射、等勢及逆函數存在性尚未附形式 Evidence。

not_formalized

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





## 下一個義務

綁定 Function.Bijective、existsUnique 與 Fintype.card／Equiv 的有限橋。





## 同源結構化資料

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

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