# 面積：半開矩形的交集、聯集與單位格重算

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-area/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-area-01 · production-20261019-adopted-96



## 目標與範圍

在等單位正交座標系中，設 A=[0,4)×[0,3)、B=[2,6)×[1,5)。求 A 與 B 的面積，求出交集 A∩B 及其面積，用包含排除求 A∪B 的面積，並以「不同單位格的個數」獨立重算。再設 C=[4,7)×[0,3)（與 A 只在 x=4 處相觸）與 Z=[3,3)×[0,5)（寬為零），求 A∩C、A∪C 的面積與 Z 的面積。

只在 MKO 的受限模型內：整數端點的半開矩形與有限個單位格的聯集。完整證明兩個半開區間的交集公式；矩形面積公式與兩矩形的包含排除取自 MKO 陳述（cited），並以單位格計數對本例獨立重算。不處理一般曲面、可測集、積分或面積的存在性，也不做 Lean 的 box volume 橋接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- order_basics
- set_operations_def
- cartesian_product_def
- finite_counting_basics


- G1 — 框架與約定：等單位正交座標系；半開約定 [a,b)={x∈ℝ ∣ a≤x<b}；端點為整數；面積單位為所用長度單位的平方（MKO 假設 a1、a3）。
- G2 — A=[0,4)×[0,3)，B=[2,6)×[1,5)。
- G3 — C=[4,7)×[0,3)，Z=[3,3)×[0,5)。


- [a,b) — 半開區間 {x ∣ a≤x<b}
- [x_0,x_1)\times[y_0,y_1) — 半開矩形
- \operatorname{area}(S) — S 的面積（平方單位）
- Q_{i,j} — 單位格 [i,i+1)×[j,j+1)
- \max,\ \min — 兩數中較大、較小者





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- 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。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- mko_area_def · cited — 在等單位正交座標系，半開矩形 [x0,x1)×[y0,y1)（x0≤x1、y0≤y1）面積為 (x1−x0)(y1−y0)。任一邊長零時矩形為空、面積零。整數單位格 [i,i+1)×[j,j+1) 面積一，有限聯集面積為不同格子的個數；兩矩形聯集面積為各面積和減交集面積。 · mko-area
- max_min_def · prerequisite — max(u,v)：u≥v 時為 u，否則為 v；min(u,v)：u≤v 時為 u，否則為 v。
- cell_decomp · prerequisite — 對整數 a≤b，[a,b) 是 b−a 個兩兩不交的單位區間 [i,i+1)（i 從 a 到 b−1）的聯集；每個 x∈[a,b) 恰屬於 i=⌊x⌋ 的那一個。
- L_interval_cap · lemma — 對實數 a₀、a₁、b₀、b₁：[a₀,a₁)∩[b₀,b₁)=[max(a₀,b₀), min(a₁,b₁))；當 max(a₀,b₀)≥min(a₁,b₁) 時右邊為空集。





## 逐步主鏈

S01 · definition操作前

\operatorname{area}([x_0,x_1)\times[y_0,y_1))

操作後

(x_1-x_0)(y_1-y_0)\quad(x_0\le x_1,\ y_0\le y_1)

條件：x_0\le x_1; y_0\le y_1

規則：mko_area_def · 依賴：G1

葉節點依據：mko_area_def + def_unfold

寫出 MKO 的受限模型：端點有序的半開矩形面積是寬乘高；單位格面積一，有限個不同單位格的聯集面積是格子個數；兩矩形聯集面積是兩面積之和減交集面積。面積以平方單位計，與周長不同。



S02 · equivalent操作前

\operatorname{area}(A)

操作後

(4-0)(3-0)=12

條件：0\le 4; 0\le 3

規則：mko_area_def · 依賴：S01, G2

葉節點依據：mko_area_def + numeric_evaluation

A=[0,4)×[0,3)，端點有序（0≤4、0≤3），所以 S01 的公式適用：寬 4−0=4，高 3−0=3，面積 4·3=12 平方單位。



S03 · equivalent操作前

\operatorname{area}(B)

操作後

(6-2)(5-1)=16

條件：2\le 6; 1\le 5

規則：mko_area_def · 依賴：S01, G2

葉節點依據：mko_area_def + numeric_evaluation

B=[2,6)×[1,5)：寬 6−2=4，高 5−1=4，面積 16 平方單位。寬是右端點減左端點，不是右端點本身。



S04 · equivalent操作前

[0,4)\cap[2,6)

操作後

[\max(0,2),\ \min(4,6))=[2,4)

條件：無

規則：L_interval_cap · 依賴：G2, L_interval_cap

葉節點依據：L_interval_cap + numeric_evaluation

依引理 L_interval_cap（a₀=0、a₁=4、b₀=2、b₁=6）：兩個 x 區間的交集是 [max(0,2), min(4,6))=[2,4)。引理在 S04.1 到 S04.3 證明。



S05 · equivalent操作前

[0,3)\cap[1,5)

操作後

[\max(0,1),\ \min(3,5))=[1,3)

條件：無

規則：L_interval_cap · 依賴：G2, L_interval_cap

葉節點依據：L_interval_cap + numeric_evaluation

對 y 區間用同一引理（a₀=0、a₁=3、b₀=1、b₁=5）：交集是 [1,3)。



S06 · equivalent操作前

A\cap B

操作後

([0,4)\cap[2,6))\times([0,3)\cap[1,5))=[2,4)\times[1,3)

條件：無

規則：cartesian_product_def · 依賴：S04, S05, G2

葉節點依據：cartesian_product_def + set_operations_def + and_intro_elim

(x,y)∈A∩B ⇔ (x∈[0,4) 且 y∈[0,3)) 且 (x∈[2,6) 且 y∈[1,5)) ⇔ x∈[0,4)∩[2,6) 且 y∈[0,3)∩[1,5)。所以兩矩形的交集仍是矩形，各邊是對應區間的交集；代入 S04、S05 得 [2,4)×[1,3)。



S07 · equivalent操作前

\operatorname{area}(A\cap B)

操作後

\max(0,4-2)\cdot\max(0,3-1)=2\cdot 2=4

條件：2\le 4; 1\le 3

規則：mko_area_def · 依賴：S01, S06

葉節點依據：mko_area_def + max_min_def + numeric_evaluation

依 MKO 假設 a2，交集寬為 max(0, min(上界)−max(下界))=max(0,4−2)=2，高為 max(0,3−1)=2。外層的 max(0, ·) 保證交集為空時寬為 0，而不是負數。這裡 2≤4、1≤3，[2,4)×[1,3) 是端點有序的矩形，面積 4。



S08 · theorem_application操作前

\operatorname{area}(A\cup B)

操作後

12+16-4=24

條件：無

規則：mko_area_def · 依賴：S02, S03, S07, mko_area_def

葉節點依據：mko_area_def + numeric_evaluation

依 MKO 的兩矩形包含排除：area(A∪B)=area(A)+area(B)−area(A∩B)=12+16−4=24。交集同時被算在 A 與 B 裡，所以要扣回一次；直接相加 28 會重算交集。



S09 · equivalent操作前

A,\ B

操作後

A=\bigcup_{0\le i\le 3,\ 0\le j\le 2}Q_{i,j},\quad B=\bigcup_{2\le i\le 5,\ 1\le j\le 4}Q_{i,j}

條件：無

規則：cell_decomp · 依賴：G1, G2, cell_decomp

葉節點依據：cell_decomp + cartesian_product_def + finite_counting_basics

依 cell_decomp，[0,4) 是 i=0,1,2,3 的 [i,i+1) 之聯集，[0,3) 是 j=0,1,2 的 [j,j+1) 之聯集；兩個聯集的笛卡兒積是各對的積之聯集，所以 A 是 4·3=12 個單位格 Q_{i,j} 的聯集。同理 B 是 i∈{2,3,4,5}、j∈{1,2,3,4} 的 16 個單位格。半開約定使不同單位格兩兩不交：每個點只在 (⌊x⌋,⌊y⌋) 那一格。



S10 · equivalent操作前

A\cup B

操作後

\bigcup_{(i,j)\in I_A\cup I_B}Q_{i,j}

條件：無

規則：set_operations_def · 依賴：S09, set_operations_def

葉節點依據：set_operations_def + set_extensionality

記 I_A、I_B 為 A、B 的格子指標集合。點在 A∪B ⇔ 它在某個 (i,j)∈I_A 的格子或某個 (i,j)∈I_B 的格子中 ⇔ 它在某個 (i,j)∈I_A∪I_B 的格子中。指標以集合合併，同一格（例如 Q_{2,1}）出現在兩邊也只算一次（MKO 假設 a3：按座標去重）。



S11 · equivalent操作前

|I_A\cup I_B|

操作後

4+6+6+4+4=24

條件：無

規則：finite_counting_basics · 依賴：S10, S09, finite_counting_basics, mko_area_def

葉節點依據：finite_counting_basics + mko_area_def + numeric_evaluation

逐列（固定 j）數不同的 i：j=0 只有 A，i∈{0,1,2,3}，4 格；j=1 時 A 給 {0,1,2,3}、B 給 {2,3,4,5}，合併為 {0,1,2,3,4,5}，6 格；j=2 同樣 6 格；j=3 只有 B，{2,3,4,5}，4 格；j=4 也是 4 格。不同列互斥，所以個數相加（finite_counting_basics）得 24。依 MKO，不同單位格聯集的面積等於格數，所以 area(A∪B)=24，與 S08 一致。



S12 · implies操作前

A\cap C,\ C=[4,7)\times[0,3)

操作後

[\max(0,4),\min(4,7))=[4,4)=\varnothing,\ \operatorname{area}(A\cup C)=12+9-0=21

條件：無

規則：L_interval_cap · 依賴：G3, L_interval_cap, S01, S02

葉節點依據：L_interval_cap + mko_area_def + numeric_evaluation

x 方向：[0,4)∩[4,7)=[max(0,4), min(4,7))=[4,4)，沒有 x 滿足 4≤x<4，是空集；所以 A∩C=∅，寬 max(0,4−4)=0，交集面積 0。C 的面積是 (7−4)(3−0)=9，故 area(A∪C)=12+9−0=21。例如點 (4,1)∈C，但 4∉[0,4)，所以 (4,1)∉A：只觸邊的兩個半開矩形沒有共同點。



S13 · implies操作前

Z=[3,3)\times[0,5)

操作後

Z=\varnothing,\ \operatorname{area}(Z)=(3-3)(5-0)=0,\ \operatorname{area}(A\cup Z)=12

條件：3\le 3

規則：mko_area_def · 依賴：G1, G3, S01, S02

葉節點依據：mko_area_def + mul_zero + set_operations_def

依半開約定，[3,3) 需要 3≤x<3，沒有這樣的 x，所以 [3,3)=∅，Z=∅×[0,5)=∅。公式也給 (3−3)(5−0)=0·5=0（mul_zero）。A∪Z=A∪∅=A，面積仍是 12。高為 5 不會讓空矩形有面積（MKO：任一邊長零時矩形為空、面積零）。



S14 · implies操作前

\text{tasks of the goal}

操作後

\operatorname{area}(A\cup B)=24,\ \operatorname{area}(A\cup C)=21,\ \operatorname{area}(Z)=0

條件：無

規則：and_intro_elim · 依賴：S02, S03, S07, S08, S11, S12, S13

葉節點依據：and_intro_elim

合併：area(A)=12、area(B)=16、A∩B=[2,4)×[1,3) 面積 4、area(A∪B)=24（包含排除與單位格計數一致）、A∩C=∅ 且 area(A∪C)=21、area(Z)=0。所有面積答案的單位都是長度單位的平方。







## 局部子步與引理

S04.1 · equivalent操作前

x\in[a_0,a_1)\cap[b_0,b_1)

操作後

(a_0\le x\ \land\ b_0\le x)\ \land\ (x<a_1\ \land\ x<b_1)

條件：無

規則：set_operations_def · 依賴：set_operations_def, G1

葉節點依據：set_operations_def + and_intro_elim

依交集定義，x 屬於交集 ⇔ x∈[a₀,a₁) 且 x∈[b₀,b₁)。依半開約定（G1），每個成員關係是兩個不等式。四個合取項重新分組：兩個下界條件放一起，兩個上界條件放一起；合取可交換、可結合，所以真假不變。



S04.2 · equivalent操作前

a_0\le x\ \land\ b_0\le x

操作後

\max(a_0,b_0)\le x

條件：無

規則：case_analysis · 依賴：S04.1, max_min_def

葉節點依據：case_analysis + max_min_def + order_basics

分兩種情況（依三分律涵蓋全部）。情況 a₀≥b₀：max(a₀,b₀)=a₀。正向：由 a₀≤x 直接得到。反向：a₀≤x，且 b₀≤a₀≤x，依傳遞得 b₀≤x。情況 a₀<b₀：max(a₀,b₀)=b₀，角色互換，同理。



S04.3 · equivalent操作前

x<a_1\ \land\ x<b_1

操作後

x<\min(a_1,b_1)

條件：無

規則：case_analysis · 依賴：S04.1, S04.2, max_min_def

葉節點依據：case_analysis + max_min_def + order_basics

情況 a₁≤b₁：min(a₁,b₁)=a₁。正向直接成立；反向：x<a₁≤b₁ 給出 x<b₁。情況 a₁>b₁：min=b₁，同理。結合 S04.1、S04.2：x∈[a₀,a₁)∩[b₀,b₁) ⇔ max(a₀,b₀)≤x<min(a₁,b₁) ⇔ x∈[max(a₀,b₀), min(a₁,b₁))。若 max(a₀,b₀)≥min(a₁,b₁)，沒有 x 同時滿足兩個不等式，交集為空。S04.1 到 S04.3 合起來證得引理 L_interval_cap。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S02, S03, S07, S08, S11, S12, S13 — 目標 G：題目要求的各個面積。足夠條件 H：S02 到 S13 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S13 · premise_audit · G1, mko_area_def, mul_zero — 空集合與零面積兩件事分別由半開約定與公式得到，互相印證。
- S12 · premise_audit · L_interval_cap, mko_area_def, S02 — 依賴引理與 MKO 的包含排除；只宣稱這一對矩形的結果。
- S11 · inverse_equivalence · finite_counting_basics, numeric_evaluation — 逐列計數是把集合分成互斥部分後的精確計數（N13）；它與 S08 用的是不同方法，兩者一致。
- S10 · inverse_equivalence · set_operations_def, set_extensionality — 聯集定義是雙向的。
- S09 · inverse_equivalence · cell_decomp, cartesian_product_def, set_extensionality — 每點屬於 A 當且僅當它屬於所列某一格，兩集合相等，雙向成立。
- S08 · premise_audit · S02, S03, S07, mko_area_def — 使用的是 MKO 陳述中的公式（cited），本稿未由測度推導；S09 到 S11 以單位格計數對本例獨立重算。
- S07 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確計算（N7 到 N9），雙向成立。
- S06 · inverse_equivalence · cartesian_product_def, set_operations_def, and_intro_elim — 每一個 ⇔ 都是定義展開或合取的重新分組，雙向成立。
- S05 · inverse_equivalence · L_interval_cap, set_extensionality — 與 S04 相同，雙向成立。
- S04.3 · inverse_equivalence · max_min_def, order_basics, case_analysis — 與 S04.2 相同的雙向論證，只是換成上界與嚴格不等式。
- S04.2 · inverse_equivalence · max_min_def, order_basics, case_analysis — 每種情況兩個方向都已說明；兩種情況涵蓋所有 a₀、b₀。
- S04.1 · inverse_equivalence · set_operations_def, and_intro_elim — 交集定義與重新分組都是雙向的。
- S04 · inverse_equivalence · L_interval_cap, set_extensionality — 引理給出兩集合有相同元素（雙向），依集合外延性兩者相等。
- S03 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確整數計算（N2），雙向成立。
- S02 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確整數計算（N1），兩邊是同一個數，雙向成立。
- S01 · premise_audit · G1, mko_area_def — 此步只寫出定義與 MKO 給定的兩個規則，不推出新事實；本稿不由測度論推導這些規則。





## 錯誤控制與反例

聯集不能直接相加MKO 指出的誤解是聯集直接相加。12+16=28 把 A∩B 的 4 個單位格算了兩次；扣回一次得 24，與 S11 逐格計數一致。只有在交集面積為零時（如 A 與 C）才可以直接相加。

重複列出的格子不增加面積Q_{2,1} 同時是 A 與 B 的格子。把 A 的格子與 B 的格子串在一起數會得到 28 筆，但不同格子只有 24 個。面積數的是不同格子（按座標去重），不是列表長度。

零寬矩形沒有面積Z=[3,3)×[0,5) 的高是 5，但寬是 0，依半開約定它是空集，面積 0（S13）。不能因為某一邊非零就認為它有面積。


- area(A∪B)=12+16=28 → reject — 交集 [2,4)×[1,3) 面積 4 被算兩次；正確值 24。
- Z=[3,3)×[0,5) 的高是 5，所以面積是 5 → reject — 寬 3−3=0，Z 是空集，面積 0·5=0。
- A 與 C 沿 x=4 重疊，所以 area(A∪C)<21 → reject — 4∉[0,4)，A∩C=∅；area(A∪C)=12+9=21。
- A 的面積是 2(4+3)=14 → reject — 14 是周長；面積是 4·3=12（MKO：矩形的幾何量不是周長）。





## 結論與限制

area(A)=12，area(B)=16，A∩B=[2,4)×[1,3) 面積 4，area(A∪B)=12+16−4=24，並由 24 個不同單位格獨立重算確認。只觸邊的 C 與 A 交集為空，area(A∪C)=21；寬為零的 Z 是空集，面積 0。單位為平方單位。


- 兩矩形的包含排除與「不同單位格聯集的面積等於格數」取自 MKO 陳述，本稿未由測度論推導；S11 的逐格計數只對本例獨立重算。
- cell_decomp（以 ⌊x⌋ 把半開整數區間分成單位區間）作為前提使用，未在本稿證明。
- MKO 的 formal next（二維 box volume 與有限聯集的橋接）未做。





## 驗證及來源綁定

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


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-area-01.json)