# 有限最大值與未取到的區間上確界

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

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

derivation-mko-supremum-and-infimum-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

求 A={-2,1/3,5/2} 與 B=(0,1) 的 sup/inf，逐一核界與最小性。

普通實值、非空有界集合，排除空集、無界與 extended reals。





## 已知條件與符號


- algebra
- sets
- definition_here


- G1 — A={-2,1/3,5/2} 完整列出；B={x∈R:0<x<1}。


- \sup,\inf — 最小上界與最大下界
- \max,\min — 取到的極值





## 規則與來源


- mko_definition · cited — s=sup A需同時證s為upper bound且不大於任何其他upper bound；inf對偶。有限有理集合提供exact slice，開區間提供未取到端點的邊界。空集、無界集合與extended-real infinity不在本輪。 · mko-supremum-and-infimum
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- definition_here · prerequisite — sup 是最小上界，inf 是最大下界；只有確界是集合成員時才同時為 maximum/minimum。





## 逐步主鏈

S01 · implies操作前

-2<1/3<5/2

操作後

\forall a\in A:\ -2\le a\le5/2

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

完整三元素排序給上下界。



S02 · implies操作前

u\text{ upper bound of }A,\quad5/2\in A

操作後

u\ge5/2

條件：無

規則：sets · 依賴：G1, S01

葉節點依據：sets

每個上界必至少為已取到的最大元素。



S03 · implies操作前

\ell\text{ lower bound of }A,\quad-2\in A

操作後

\ell\le-2

條件：無

規則：sets · 依賴：G1, S01

葉節點依據：sets

每個下界不大於已取到的最小元素。



S04 · definition操作前

5/2\text{ least upper bound},\quad-2\text{ greatest lower bound}

操作後

\sup A=\max A=5/2,\quad\inf A=\min A=-2

條件：無

規則：definition_here · 依賴：S01, S02, S03

葉節點依據：definition_here

此有限集合的確界都在集合中，所以同時是最大最小。



S05 · implies操作前

x\in B\iff0<x<1

操作後

0\text{ is a lower bound and }1\text{ an upper bound}

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

區間端點提供界，但依定義兩個端點都不在 B。



S06 · implies操作前

u<1

操作後

x=(1+\max\{u,0\})/2\in B,\quad x>u

條件：u<1

規則：algebra · 依賴：G1, S05

葉節點依據：algebra

max 讓任意 u<1（含負 u）都有合法 B 成員超過它，所以 u 不可能是上界。



S07 · implies操作前

\ell>0

操作後

x=\min\{\ell,1\}/2\in B,\quad x<\ell

條件：\ell>0

規則：algebra · 依賴：G1, S05

葉節點依據：algebra

任意正候選下界都被一個更小 B 成員否定。



S08 · definition操作前

1\text{ least upper bound},\quad0\text{ greatest lower bound},\quad0,1\notin B

操作後

\sup B=1,\quad\inf B=0;\quad B\text{ has no maximum or minimum}

條件：無

規則：definition_here · 依賴：S05, S06, S07

葉節點依據：definition_here

確界存在但未取到；若有最大最小，它們必等於已證唯一確界，與不在集合矛盾。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S05, S06, S07 — 未將未取到端點誤判為無確界。
- S07 · premise_audit · G1, S05 — ell≥1 與 0<ell<1 兩種情況均被 min 公式涵蓋。
- S06 · premise_audit · G1, S05 — 構造同時核 0<x<1 與 x>u，不只靠圖形。
- S05 · premise_audit · G1 — 不把 ≤ 的界條件與 < 的成員條件混同。
- S04 · premise_audit · S01, S02, S03 — 成員資格已另核，不普遍假定 sup 是成員。
- S03 · premise_audit · G1, S01 — 方向是下界≤最小值，不是相反。
- S02 · premise_audit · G1, S01 — 上界與最小性各自核，不能只證一個。
- S01 · premise_audit · G1 — 沒有未列出的 A 成員。





## 錯誤控制與反例

兩個責任每個確界都需界條件與極小／極大性。

取到另核只有確界是成員才稱最大或最小。


- B 的最大元素是 1。 → reject — 1 不在 B。
- 2 是 B 的 supremum，因為它是上界。 → reject — 不是最小上界，1 更小且仍是上界。
- 空集也依同一普通實數規則有最大元素。 → reject — 沒有成員可取；本稿明確排除空集合版本。





## 結論與限制

A 的 sup=5/2、inf=-2 且都取到；B 的 sup=1、inf=0 但都不取到。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 032fe27da01180f3cc81291f7ffabfb4d24f950b41d70acba163555cd43e319d
- original source SHA-256: 5943c7e129fd8edd4ae73e3d131e0463a489f64dc39ea5e81897df1c99ccccf8
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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