圓的邊界與座標判定

數學敘述

在歐氏平面固定中心 O 與半徑 r≥0，C(O,r)={P:d(P,O)=r}；r>0 是通常的非退化圓，r=0 是僅含 O 的退化點集。點距中心小於、等於、大於 r 分別判為內、圓上、外；直徑長為 2r。

代表公式（精確 TeX）

C(O,r)

成立條件

• 座標題與距離條目同採等單位正交框架，整數中心、點及非負整數半徑。
• 負半徑不在本輪論域；r=0 沒有內部，中心在圓上。
• 軸向點 O±(r,0) 或 O±(0,r) 均在圓上；r=0 時四種表示是同一點。

符號作用域

• C — 圓邊界點集
• O — 圓心
• r — 非負半徑

直觀、定義與常見誤解

對 r≥0，可把 d(P,O)=r 等價改成距離平方等於 r²；小於與大於同樣由非負平方比較。圓內的點不是圓邊界的成員。

r=0 時只中心滿足等距條件；其他點都在外，直徑為零。本輪特別稱它退化點集，不混稱正半徑曲線。

軸向座標點以明示方向精確構造，不依螢幕圖形目測。圓心平移對成員判定不構成新計算，直徑題也不靠無關圓心變化充量。

把圓當圓盤，接受負半徑，或在零半徑判出內部點。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 歐幾里得長度 — 半徑及直徑使用長度單位。
• 點、線、面 — 圓是平面中的點集。
• 等單位正交座標的歐氏距離 — 整數座標判定比較平方距離。

驗證界線

整數半徑及座標判定可重算；一般圓、圓盤與球面 API 的形式橋仍待建立。

not_formalized

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

下一個義務

綁定 EuclideanSpace 上 Metric.sphere／ball，分開正半徑與零半徑。

同源結構化資料

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