完整映射表的基數證書

目標與範圍

有單射A→B且|A|=2<3=|B|；反向滿射非單射。

只處理明示有限集合與完整映射，不作無限選擇主張。

已知條件與符號

• calc

• G1 — A={a,b}，B={1,2,3}；f(a)=1,f(b)=2；g(1)=a,g(2)=b,g(3)=a。

• f,g — 方向不同的映射
• A,B,C — 完整有限集合

規則與來源

• calc · prerequisite — 假設有限集合計數、單射與滿射的定義。
• mko_definition · cited — 本輪限完整有限集合。A到B單射證|A|<=|B|，滿射證|A|>=|B|，雙射證相等；若|A|>|B|則不存在單射。無限集合的surjection逆向比較需要額外choice／section責任，不在本輪。 · mko-cardinality-comparison

逐步主鏈

A=\{a,b\},\ B=\{1,2,3\}

|A|=2,\quad |B|=3

f:A\to B

\operatorname{graph}(f)=\{(a,1),(b,2)\}

f(a)=1,\ f(b)=2

f(a)\ne f(b)\Rightarrow f\text{ injective}

f(A)=\{1,2\}

3\notin f(A),\quad f\text{ not surjective},\quad 2\le3

g:B\to A

g^{-1}(\{a\})=\{1,3\},\quad g^{-1}(\{b\})=\{2\}

g(B)=A,\quad g(1)=g(3)

g\text{ surjective but not injective};\quad3\ge2

h:B\to A\text{ assumed injective}

h(1),h(2),h(3)\text{ distinct in a two-element set: impossible}

C=\{u,v\},\quad b(a)=u,\ b(b)=v

b:A\to C\text{ bijective};\quad |A|=|C|=2

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S01 — 等式有具體雙射支撐，並未把原來的f誤稱滿射。
• S07 · premise_audit · G1, S01 — 這否證所有h，不只是g；理由依完整載體數目。
• S06 · premise_audit · G1, S05 — 滿射與單射分開判斷；反向滿射只給有限基數反向不等式。
• S05 · premise_audit · G1 — fiber是來源元素集合，不能把輸入1與3合併為一個元素。
• S04 · premise_audit · G1, S01, S03 — 不可把單射錯寫成雙射；缺像已由完整來源表證實。
• S03 · premise_audit · G1, S02 — 1≠2是在B內的相異性；單射並不要求命中3。
• S02 · premise_audit · G1, S01 — 不可只檢查已填表格而遺漏一個來源元素。
• S01 · premise_audit · G1 — 先固定集合；同一映射換codomain可能改變滿射性。

錯誤控制與反例

總表

f須有兩個entries，g須有三個；來源長度不可混用。

比較方向

單射A→B給|A|≤|B|，滿射同方向給≥。

• f是雙射。 → reject — 3沒有前像。
• g是單射。 → reject — g(1)=g(3)=a且1≠3。
• 由這兩個有限例子已證無限滿射都有section。 → reject — 證書只涵蓋A、B、C，未處理無限集合或選擇原理。

結論與限制

有單射A→B且|A|=2<3=|B|；反向滿射非單射。

驗證及來源綁定

1 個本稿宣告算術檢查；只支持所列算式。

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: f7395fd1e6ecb7e29d7182b804fa89d6a0e5440629fc2b259fbe84acd59ce55b
• original source SHA-256: f7395fd1e6ecb7e29d7182b804fa89d6a0e5440629fc2b259fbe84acd59ce55b
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）