# 座標矩形與單位格的面積

先精確處理半開矩形及有限單位格聯集，含重疊、觸邊與空矩形；不冒充一般面積理論。

mko-area · definition · v0.10.0



## 數學敘述

在等單位正交座標系，半開矩形 [x0,x1)×[y0,y1)（x0≤x1、y0≤y1）面積為 (x1−x0)(y1−y0)。任一邊長零時矩形為空、面積零。整數單位格 [i,i+1)×[j,j+1) 面積一，有限聯集面積為不同格子的個數；兩矩形聯集面積為各面積和減交集面積。





## 代表公式（精確 TeX）

A(w,h)





## 成立條件


- 題庫採非負整數邊長或有序整數端點；半開端點及同單位框架須明示。
- 兩矩形交集寬高分別為 max(0,min(上界)−max(下界))；相離與僅觸邊交集面積零。
- 單位格按座標去重，重複列格不增加面積；答案單位為所用長度單位的平方。





## 符號作用域


- A — 本輪矩形面積運算
- w — 非負寬
- h — 非負高





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

矩形的幾何量不是周長。兩矩形有重疊時直接相加會重算交集，必須扣回一次；相同矩形的聯集仍只有原面積。

整數半開框架可把矩形分成不重複的單位格，提供與包含排除不同的有限重算方法。空矩形及空格子聯集面積都是零。

本輪只建立矩形與有限格子的候選模型，不宣稱一般曲面、可測集、積分或面積存在性已驗證。共同平移或交換兩矩形只是同一計算的表示變動。

聯集直接相加、把重複格子重算，或把零寬矩形當有面積。





## 已採用的推導導讀

[面積：半開矩形的交集、聯集與單位格重算](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-area-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [歐幾里得長度](https://ocme.evemisslab.com/zh-Hant/mko/mko-euclidean-length/) — 固定長度單位及正交框架。
- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 精確長乘寬與加減。
- [座標平面](https://ocme.evemisslab.com/zh-Hant/mko/mko-coordinate-plane/) — 矩形端點和單位格位置。
- [集合運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-operations/) — 聯集、交集及表示去重。





## 驗證界線

有限矩形／格子面積可精確重算；一般 Lebesgue 面積及積分橋未新增形式 Evidence。

not_formalized

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





## 下一個義務

在固定版橋接二維 box volume、空邊界與有限聯集；先維持本輪受限模型。





## 同源結構化資料

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

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