# 二元關係與集合投影

二元關係是指定 A×B 中有序對的集合，不要求每個輸入唯一或必有輸出。

mko-relation · definition · v0.10.0



## 數學敘述

對集合 A、B，從 A 到 B 的二元關係 R 是 A×B 的子集合；xRy 表示 (x,y)∈R。關係定義域 Dom(R)={x∈A:存在 y∈B，使 (x,y)∈R}，關係像 R[C]={y∈B:存在 x∈C，使 (x,y)∈R}，逆關係 R⁻¹={(y,x):(x,y)∈R}⊆B×A。





## 代表公式（精確 TeX）

R(x,y)





## 成立條件


- 來源 A、目標 B 和關係 R 已明示；C 是 A 的子集合。
- 有序對保留方向；本輪題庫是有限整數集合與有序對資料。





## 符號作用域


- R — 指定二元關係
- x — 第一分量
- y — 第二分量





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

R 不必是總函數：一個第一分量可沒有或具有多個第二分量。把 R⊆A×B 的宣告來源 A 叫成 Dom(R) 會漏掉實際第一投影的差異。

R[C] 只收集從 C 中元素連到的輸出，重複值只列一次。空關係與空輸入集合的像均為空。

逆關係交換有序對方向並交換來源／目標；它不自動是反函數，也不提供單射、滿射或可逆性的證明。

把宣告來源集合當成實際關係定義域，或把逆關係當成已存在的反函數。





## 已採用的推導導讀

[二元關係：定義域、關係像與逆關係的逐步計算](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-relation-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合隸屬](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-membership/) — 關係和有序對成員需用成員語義。
- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 來源、目標、投影與像都是集合。





## 驗證界線

明示有限關係可完整枚舉；一般關係性質及函數特殊化仍待形式化。

not_formalized

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





## 下一個義務

綁定 Set (A×B)、第一投影、關係像及 converse；函數條件保持為額外限制。





## 同源結構化資料

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

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