# 完整映射表的基數證書 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-cardinality-comparison/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-cardinality-comparison-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 有單射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 ## 逐步主鏈 S01 · implies操作前 A=\{a,b\},\ B=\{1,2,3\} 操作後 |A|=2,\quad |B|=3 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 來源與目標均完整且內部元素互異，計數無重複。 S02 · implies操作前 f:A\to B 操作後 \operatorname{graph}(f)=\{(a,1),(b,2)\} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 兩個來源元素恰各有一個像，像都在B中，因此f是總映射。 S03 · implies操作前 f(a)=1,\ f(b)=2 操作後 f(a)\ne f(b)\Rightarrow f\text{ injective} 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc A只有兩個元素，唯一不同元素對的像不同，已核全部碰撞。 S04 · implies操作前 f(A)=\{1,2\} 操作後 3\notin f(A),\quad f\text{ not surjective},\quad 2\le3 條件：無 規則：mko_definition · 依賴：G1, S01, S03 葉節點依據：mko_definition 缺少3否證滿射；兩個不同像仍給|A|≤|B|證書。 S05 · implies操作前 g:B\to A 操作後 g^{-1}(\{a\})=\{1,3\},\quad g^{-1}(\{b\})=\{2\} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 完整反向表給兩個非空fiber，全部B都已列入。 S06 · implies操作前 g(B)=A,\quad g(1)=g(3) 操作後 g\text{ surjective but not injective};\quad3\ge2 條件：無 規則：mko_definition · 依賴：G1, S05 葉節點依據：mko_definition a、b均有前像，所以g滿射；1≠3但像同，故非單射。 S07 · implies操作前 h:B\to A\text{ assumed injective} 操作後 h(1),h(2),h(3)\text{ distinct in a two-element set: impossible} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 單射會要求A內三個互異元素；A明列只有兩個，所以任何反向單射都不存在。 S08 · implies操作前 C=\{u,v\},\quad b(a)=u,\ b(b)=v 操作後 b:A\to C\text{ bijective};\quad |A|=|C|=2 條件：無 規則：mko_definition · 依賴：G1, S01 葉節點依據：mko_definition 另列完整雙射：不同來源像不同，且u、v皆命中，給相等基數證書。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-cardinality-comparison-01.json)