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

目標與範圍

求 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。

逐步主鏈

-2<1/3<5/2

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

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

u\ge5/2

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

\ell\le-2

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

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

x\in B\iff0<x<1

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

u<1

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

\ell>0

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

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}

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）