可測函數：以完整列舉逐一核逆像，並以合成、指示函數與像集陷阱對照

目標與範圍

X={0,1,2,3}、Σ_X={∅,{0,1},{2,3},X}；Y={0,1,2}、Σ_Y={∅,{0},{1,2},Y}；Z={0,1}、Σ_Z 為冪集。(1) 以完整列舉證明 f=(0↦0,1↦0,2↦1,3↦2) 可測，而 g=(0↦0,1↦1,2↦1,3↦2) 不可測；(2) 證明可測映射的合成可測，並把 φ∘f 讀回為指示函數；(3) 證明指示函數 1_E 可測若且唯若 E∈Σ_X；(4) 用 m 與 k 說明「檢查像集」既會誤拒也會誤收。

只處理 G1 到 G5 指定的有限可測空間與完整總映射表（MKO 假設 a1）。完整有限列舉只證這些實例；合成引理與指示函數引理對任意可測空間證明。可測不推出連續、可積或保測（a2）。不改動 canonical MKO 或其英文 edition。

已知條件與符號

• image_preimage_def
• set_operations_def
• function_def
• composition_def
• set_extensionality

• G1 — X={0,1,2,3}，Σ_X={∅,{0,1},{2,3},X}。
• G2 — Y={0,1,2}，Σ_Y={∅,{0},{1,2},Y}。
• G3 — 完整映射表：f(0)=0、f(1)=0、f(2)=1、f(3)=2；g(0)=0、g(1)=1、g(2)=1、g(3)=2。
• G4 — Z={0,1}，Σ_Z={∅,{0},{1},Z}；φ:Y→Z，φ(0)=0、φ(1)=1、φ(2)=1。
• G5 — 像集陷阱例子：m:X→Y，m(0)=0、m(1)=0、m(2)=1、m(3)=1；k:X→Z，k(0)=0、k(1)=1、k(2)=1、k(3)=1。

• (X,\Sigma_X) — 來源可測空間，X={0,1,2,3}
• (Y,\Sigma_Y) — 目標可測空間，Y={0,1,2}
• (Z,\Sigma_Z) — Z={0,1}，Σ_Z 為冪集
• f,g,m:X\to Y — 待檢的總映射
• \varphi:Y\to Z,\ k:X\to Z — 合成用映射與像集陷阱例子
• u^{-1}(B) — 逆像 {x ∣ u(x)∈B}
• \mathbf{1}_E — E 的指示函數

規則與來源

• image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_measurable_def · cited — 給有限可測空間 (X,Σ_X) 與 (Y,Σ_Y)，總函數 f:X→Y 可測，若每個 B∈Σ_Y 的逆像 f⁻¹(B) 都屬 Σ_X。本輪用完整有限列舉逐一核逆像。 · mko-measurable-function
• mko_sigma_def · cited — 在集合 X 上，σ-代數含空集，對補集及可數聯集封閉；完整有限載體可把可數責任歸約為有限多個相異集合。 · mko-sigma-algebra-measure-space
• p_indicator_def · prerequisite — 對 E⊆X，指示函數 1_E:X→{0,1}：x∈E 時 1_E(x)=1，否則 1_E(x)=0。
• L_comp_meas · lemma — 對任意可測空間，若 u:(A,𝒜)→(B,ℬ) 與 ψ:(B,ℬ)→(C,𝒞) 可測，則 (ψ∘u)⁻¹(D)=u⁻¹(ψ⁻¹(D)) 對每個 D⊆C 成立，且 ψ∘u 可測。
• L_indicator · lemma — 對任意可測空間 (X,Σ) 與 E⊆X，以 {0,1} 的冪集為目標 σ-代數時，1_E 可測 ⇔ E∈Σ。

逐步主鏈

u:(X,\Sigma_X)\to(Y,\Sigma_Y)\ \text{measurable}

\forall B\in\Sigma_Y:\ u^{-1}(B)\in\Sigma_X

\Sigma_X,\ \Sigma_Y,\ \Sigma_Z

\text{each is a}\ \sigma\text{-algebra on its carrier}

f:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto2

f:X\to Y\ \text{total}

u:X\to Y\ \text{total}

u^{-1}(\emptyset)=\emptyset\in\Sigma_X,\quad u^{-1}(Y)=X\in\Sigma_X

f^{-1}(\{0\})

\{x\mid f(x)=0\}=\{0,1\}\in\Sigma_X

f^{-1}(\{1,2\})

\{x\mid f(x)\in\{1,2\}\}=\{2,3\}\in\Sigma_X

B\in\{\emptyset,\{0\},\{1,2\},Y\}

f^{-1}(B)\in\Sigma_X\ \text{for every}\ B\in\Sigma_Y:\ f\ \text{measurable}

g^{-1}(\{0\})

\{0\}\notin\Sigma_X:\ g\ \text{not measurable}

u,\ \psi\ \text{measurable}

(\psi\circ u)^{-1}(D)=u^{-1}(\psi^{-1}(D)),\ \ \psi\circ u\ \text{measurable}

\varphi:\ 0\mapsto0,\ 1\mapsto1,\ 2\mapsto1

\varphi^{-1}(\{0\})=\{0\},\ \varphi^{-1}(\{1\})=\{1,2\}\in\Sigma_Y:\ \varphi\ \text{measurable}

\varphi\circ f

\varphi\circ f:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto1,\ \ \text{measurable}

\mathbf{1}_E:(X,\Sigma)\to(\{0,1\},\mathcal{P}(\{0,1\}))

\mathbf{1}_E\ \text{measurable}\iff E\in\Sigma

\varphi\circ f=\mathbf{1}_{\{2,3\}},\ k=\mathbf{1}_{\{1,2,3\}}

\mathbf{1}_{\{2,3\}}\ \text{measurable};\ \mathbf{1}_{\{0\}},\ k\ \text{not measurable}

m:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto1

m\ \text{measurable, yet}\ m(\{2,3\})=\{1\}\notin\Sigma_Y

k:X\to Z,\ \Sigma_Z=\mathcal{P}(Z)

k(A)\in\Sigma_Z\ \text{for every}\ A\in\Sigma_X,\ \text{yet}\ k^{-1}(\{0\})=\{0\}\notin\Sigma_X

\text{S07 to S15}

f,\ \varphi,\ \varphi\circ f,\ m\ \text{measurable};\ g,\ k\ \text{not}

局部子步與引理

\Sigma_X=\{\emptyset,\{0,1\},\{2,3\},X\}

\emptyset\in\Sigma_X;\ \emptyset^c=X,\ \{0,1\}^c=\{2,3\};\ \{0,1\}\cup\{2,3\}=X

\Sigma_Y=\{\emptyset,\{0\},\{1,2\},Y\},\ \Sigma_Z=\mathcal{P}(Z)

\Sigma_Y,\ \Sigma_Z\ \text{are}\ \sigma\text{-algebras}

x\in(\psi\circ u)^{-1}(D)

x\in u^{-1}(\psi^{-1}(D))

D\in\mathcal{C}

\psi^{-1}(D)\in\mathcal{B}\ \Rightarrow\ u^{-1}(\psi^{-1}(D))\in\mathcal{A}

\mathbf{1}_E^{-1}(C),\ C\subseteq\{0,1\}

\emptyset\mapsto\emptyset,\ \{1\}\mapsto E,\ \{0\}\mapsto X\setminus E,\ \{0,1\}\mapsto X

\{\emptyset,E,X\setminus E,X\}\subseteq\Sigma

\iff E\in\Sigma

逐步反向審查

• S16 · premise_audit · S07, S08, S11, S13 — 只合取已證結論；這些結論只針對 G1 到 G5 的實例，兩個引理則對一般可測空間成立。
• S15 · premise_audit · image_preimage_def, S13 — 兩個反例各否定一個方向的蘊含。
• S14 · premise_audit · image_preimage_def, S04 — 可測性由逆像決定；像集不在 Σ_Y 中與可測性無關。
• S13 · premise_audit · L_indicator, G1 — 判定 E 是否在 Σ_X 中，只需與 Σ_X 的四個成員逐一比較。
• S12.2 · inverse_equivalence · iff_intro, mko_sigma_def — 兩個方向都有理由：⇒ 用一個逆像，⇐ 用 σ-代數的補集封閉。
• S12.1 · inverse_equivalence · p_indicator_def, image_preimage_def — 四個逆像都由定義雙向確定。
• S12 · premise_audit · L_indicator — 目標 σ-代數取冪集；若目標只取 {∅,{0,1}}，任何函數都可測，引理的形式會不同。
• S11 · premise_audit · L_comp_meas, S07, S10 — 引理的兩個前提都已核；直接讀回是獨立的交叉核對。
• S10 · premise_audit · image_preimage_def, case_analysis — 完整列舉 Σ_Z 的四個成員。
• S09.2 · premise_audit · S09.1, forall_elim, forall_intro — 兩次代入特例；中間集合 ψ⁻¹(D) 必須在 ℬ 中，u 的可測性才能用上。
• S09.1 · inverse_equivalence · image_preimage_def, composition_def, set_extensionality — 整條鏈雙向成立；不需要任何映射可逆。
• S09 · premise_audit · L_comp_meas — 需要兩個映射各自可測；只有其中一個可測時不宣稱。
• S08 · premise_audit · quantifier_negation, image_preimage_def — 否定全稱只需一個反例 B={0}；g 與 f 只差 g(1)，但這就足以破壞可測性。
• S07 · premise_audit · S04, S05, S06, case_analysis — 這是有限全稱的完整驗證，只證這一個 f（MKO 假設 a2）。
• S06 · inverse_equivalence · image_preimage_def, set_extensionality — 完整列舉；兩種算法結果一致，可互相核對。
• S05 · inverse_equivalence · image_preimage_def, set_extensionality — 四個點全部檢查，逆像集合由定義雙向確定。
• S04 · premise_audit · image_preimage_def, function_def — u⁻¹(Y)=X 用到 u 是總函數；部分函數會使這一步失敗。
• S03 · premise_audit · function_def, G3 — 若表缺一個點，逆像就無法完整計算；全部 4 個點都列出了。
• S02.2 · premise_audit · set_operations_def, G2, G4 — 冪集永遠是 σ-代數；Σ_Y 的核對與 S02.1 逐項對應。
• S02.1 · premise_audit · set_operations_def, G1 — C(4,2)=6 對聯集全部涵蓋（N1）；有限族的可數聯集等於有限聯集。
• S02 · premise_audit · mko_sigma_def — 有限歸約只對有限族有效；這裡三個族各有 4 個成員。
• S01 · premise_audit · mko_measurable_def — 只展開定義；方向是逆像，不是像（見 S14、S15）。

錯誤控制與反例

檢查逆像，不是像集

MKO 指出的誤解之一是檢查像集而非逆像。S14 的 m 可測，但像集 m({2,3})={1} 不在 Σ_Y 中；S15 的 k 所有像集都在 Σ_Z 中，卻因 k⁻¹({0})={0}∉Σ_X 而不可測。可測性的方向是：目標可測集取逆像，回到來源 σ-代數。

可測不是保測

MKO 假設 a2 提醒可測不推出連續、可積或保測。例如在 Σ_X 上取 μ_X({0,1})=μ_X({2,3})=1/2、在 Σ_Y 上取 μ_Y({0})=1/3、μ_Y({1,2})=2/3（兩者都由原子權重給出，總和 1，N3、N4），f 可測，但 μ_X(f⁻¹({0}))=μ_X({0,1})=1/2≠1/3=μ_Y({0})（N5），所以 f 不保測。

先核 σ-代數，再談可測

可測性的定義預設兩邊都是 σ-代數（S02）。若把 Σ_X 誤寫成 {∅,{0,1},X}（缺 {0,1} 的補集 {2,3}），它就不是 σ-代數，S06 的結論「f⁻¹({1,2})={2,3}∈Σ_X」也會失敗；問題出在集合族而不是函數。

• m({2,3})={1} 不在 Σ_Y 中，所以 m 不可測 → reject — 可測性看逆像：m⁻¹({0})={0,1}、m⁻¹({1,2})={2,3} 都在 Σ_X 中（S14）。
• k 的每個像集都在 Σ_Z 中，所以 k 可測 → reject — k⁻¹({0})={0}∉Σ_X（S15）。
• g 與 f 只在一個點不同，所以 g 也可測 → reject — g⁻¹({0})={0}∉Σ_X（S08）；可測性對單點改動並不穩定。
• f 可測，所以對任何測度 μ_X、μ_Y 都有 μ_X(f⁻¹(B))=μ_Y(B) → reject — 錯誤控制 2 的測度給 1/2≠1/3；可測不推出保測。

結論與限制

f 可測（f⁻¹({0})={0,1}、f⁻¹({1,2})={2,3}）；g 不可測（g⁻¹({0})={0}∉Σ_X）。合成可測映射可測，φ∘f=1_{{2,3}} 可測；1_E 可測 ⇔ E∈Σ_X，故 1_{{0}} 與 k=1_{{1,2,3}} 不可測。m 可測但 m({2,3})={1}∉Σ_Y，k 的像全在 Σ_Z 中卻不可測：像集檢查不能代替逆像檢查。

• 錯誤控制 2 的 μ_X、μ_Y 以原子權重給出；它們是測度的事實沿用 σ-代數與測度空間條目的原子構造，未在本稿重證。
• 簡單函數、積分與測度收斂（MKO 的 formal next）不在範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: b30cc3fb4fd89f6219b80c50db6bfa4bdd2524d76e965a40117637009646bdf0
• original source SHA-256: b30cc3fb4fd89f6219b80c50db6bfa4bdd2524d76e965a40117637009646bdf0
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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