# 實數的通常順序：加法保序、正分母交叉比較、有限極值與閉區間

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

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

derivation-mko-order-relation-01 · production-20261019-adopted-96



## 目標與範圍

證明對所有實數 a、b、c：a<b ⇔ a+c<b+c；q、s>0 時 p/q<r/s ⇔ ps<rq；非空有限實數集合有最小元素，且最小元素唯一。據此比較 M={−5/9, 1/3, −7/12, −1/2}（照此次序列出）的元素，求 M 的最小與最大元素，並判定兩端點與 1/2 是否屬於閉區間 [min M, max M]。

只談實數的通常全序（MKO a1），以 order_basics 中的順序公理為前提，不構造實數。比較題使用正分母有理數（a2）；極值只對非空有限集合，閉區間要求下界不大於上界（a3）。最大元素的存在以「同一論證把 ≤ 換成 ≥」帶過。不處理複數、一般偏序或無限集合的上確界；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- frac_rules
- add_inverse
- nat_induction
- numeric_evaluation


- G1 — ℝ 上的通常順序 ≤ 自反、反對稱、傳遞，且任兩數可比較；a<b 表示 a≤b 且 a≠b。
- G2 — M={−5/9, 1/3, −7/12, −1/2}，依此次序列出；寫成正分母形式：(−5)/9、1/3、(−7)/12、(−1)/2。
- G3 — 定義：m 是集合 M 的最小元素，指 m∈M 且對所有 x∈M 有 m≤x；最大元素同理以 ≥。對 l≤u，閉區間 [l,u]={x∈ℝ ∣ l≤x 且 x≤u}。


- a\le b,\ a<b — 通常順序與嚴格順序
- \frac{p}{q} — 有理數，分母 q>0
- M — 待比較的有限集合
- \min M,\ \max M — 最小與最大元素
- [l,u] — 閉區間 {x ∣ l≤x≤u}





## 規則與來源


- 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。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_order · cited — 實數的通常順序 ≤ 滿足自反、反對稱、傳遞及任兩數可比較；a<b 表示 a≤b 且 a≠b。任意實數 a、b、c 都有 a<b 當且僅當 a+c<b+c。非空有限實數集合有最小與最大元素；閉區間 [l,u]（l≤u）包含兩端點。 · mko-order-relation
- min_max_def · prerequisite — 最小元素：m∈M 且 ∀x∈M, m≤x；最大元素：m∈M 且 ∀x∈M, m≥x。
- interval_def · prerequisite — 閉區間：對 l≤u，x∈[l,u] ⇔ l≤x 且 x≤u。
- L_translate · lemma — 對所有實數 a、b、c：a<b ⇔ a+c<b+c。
- L_cross · lemma — 對實數 p、r 與 q>0、s>0：p/q<r/s ⇔ ps<rq。
- L_finite_min · lemma — 每個非空有限實數集合都有最小元素。
- L_min_unique · lemma — 一個實數集合至多有一個最小元素（最大元素同理）。





## 逐步主鏈

S01 · definition操作前

a,b\in\mathbb{R}

操作後

a<b\ :\iff\ a\le b\land a\neq b;\ \text{exactly one of}\ a<b,\ a=b,\ b<a

條件：無

規則：mko_order · 依賴：G1, mko_order

葉節點依據：mko_order + order_basics

依 MKO 定義嚴格順序。由全序性（a≤b 或 b≤a）與反對稱（兩者同時成立則 a=b）可得三分律：a<b、a=b、b<a 恰有一個成立。這就是 MKO 所說的三分比較輸出 <、= 或 >。



S02 · equivalent操作前

a<b

操作後

a+c<b+c

條件：無

規則：L_translate · 依賴：S01

葉節點依據：order_basics + add_assoc + add_inverse + add_zero

依引理 L_translate，兩數同加 c 不改變比較。⇒ 在 S02.1，⇐ 在 S02.2。



S03 · equivalent操作前

\frac{p}{q}<\frac{r}{s}

操作後

ps<rq

條件：q>0; s>0

規則：L_cross · 依賴：S01

葉節點依據：order_basics + frac_rules + mul_inverse_nonzero

依引理 L_cross：分母都為正時，比較兩個分數等於比較交叉乘積。證明在 S03.1 至 S03.3；正分母條件不可省略。



S04 · equivalent操作前

-\tfrac{7}{12}\ ?\ -\tfrac{5}{9}

操作後

(-7)\cdot9=-63<-60=(-5)\cdot12\ \Rightarrow\ -\tfrac{7}{12}<-\tfrac{5}{9}

條件：12>0; 9>0

規則：L_cross · 依賴：S03, G2

葉節點依據：order_basics + numeric_evaluation

取 p=−7、q=12、r=−5、s=9，分母都為正。ps=−63、rq=−60，而 −60−(−63)=3>0，所以 −63<−60；依 L_cross，−7/12<−5/9。



S05 · equivalent操作前

-\tfrac{5}{9}\ ?\ -\tfrac{1}{2}

操作後

(-5)\cdot2=-10<-9=(-1)\cdot9\ \Rightarrow\ -\tfrac{5}{9}<-\tfrac{1}{2}

條件：9>0; 2>0

規則：L_cross · 依賴：S03, G2

葉節點依據：order_basics + numeric_evaluation

取 p=−5、q=9、r=−1、s=2：ps=−10、rq=−9，−10<−9，所以 −5/9<−1/2。



S06 · equivalent操作前

-\tfrac{1}{2}\ ?\ \tfrac{1}{3}

操作後

(-1)\cdot3=-3<2=1\cdot2\ \Rightarrow\ -\tfrac{1}{2}<\tfrac{1}{3}

條件：2>0; 3>0

規則：L_cross · 依賴：S03, G2

葉節點依據：order_basics + numeric_evaluation

取 p=−1、q=2、r=1、s=3：ps=−3、rq=2，−3<2，所以 −1/2<1/3。



S07 · implies操作前

-\tfrac{7}{12}<-\tfrac{5}{9},\ -\tfrac{5}{9}<-\tfrac{1}{2},\ -\tfrac{1}{2}<\tfrac{1}{3}

操作後

-\tfrac{7}{12}<-\tfrac{5}{9}<-\tfrac{1}{2}<\tfrac{1}{3}

條件：無

規則：order_basics · 依賴：S04, S05, S06

葉節點依據：order_basics + logic_chain

三個比較串成一條鏈；依 < 的傳遞性，鏈上任一數小於它右邊的每一個數，例如 −7/12<−1/2、−7/12<1/3、−5/9<1/3。M 的四個元素就此全部排好。



S08 · implies操作前

M\subseteq\mathbb{R}\ \text{finite},\ M\neq\varnothing

操作後

M\ \text{has a minimum}

條件：M\neq\varnothing

規則：L_finite_min · 依賴：S01

葉節點依據：nat_induction + order_basics + case_analysis

MKO 斷言非空有限實數集合有最小與最大元素。依引理 L_finite_min，對元素個數 n≥1 歸納證明最小元素存在（S08.1、S08.2）；最大元素的論證相同，只需把 ≤ 換成 ≥。



S09 · implies操作前

-\tfrac{7}{12}\in M,\ -\tfrac{7}{12}\le x\ \forall x\in M

操作後

\min M=-\tfrac{7}{12}

條件：無

規則：min_max_def · 依賴：S07, G2, min_max_def

葉節點依據：min_max_def + order_basics

−7/12 屬於 M（列在第三個），由 S07 它小於其餘三個元素，對自己則 −7/12≤−7/12，所以它是最小元素。M 列出時 −5/9 排在第一，但極值由值決定，不由列出次序決定。



S10 · implies操作前

\tfrac{1}{3}\in M,\ \tfrac{1}{3}\ge x\ \forall x\in M

操作後

\max M=\tfrac{1}{3}

條件：無

規則：min_max_def · 依賴：S07, G2, min_max_def

葉節點依據：min_max_def + order_basics

1/3 屬於 M，由 S07 其餘三個元素都小於 1/3，所以 1/3 是最大元素。



S11 · implies操作前

m,m'\ \text{both minima of}\ M

操作後

m=m'

條件：無

規則：L_min_unique · 依賴：S09, S10

葉節點依據：min_max_def + order_basics

依引理 L_min_unique，最小元素唯一，所以可以說「這個」最小元素 −7/12；最大元素 1/3 同理唯一。證明在 S11.1。



S12 · implies操作前

l=-\tfrac{7}{12},\ u=\tfrac{1}{3}

操作後

l\le u

條件：無

規則：order_basics · 依賴：S07, S09, S10, G3

葉節點依據：order_basics + mko_order

MKO 假設 a3 要求先驗閉區間的下界不大於上界。由 S07，l=−7/12<1/3=u，故 l≤u，[l,u] 是合法的閉區間。



S13 · implies操作前

l\le l\le u,\ l\le u\le u

操作後

l\in[l,u],\ u\in[l,u],\ M\subseteq[l,u]

條件：l\le u

規則：interval_def · 依賴：S12, S09, S10, interval_def

葉節點依據：interval_def + mko_order

閉區間的成員條件是 l≤x≤u。對 x=l：l≤l（自反）且 l≤u（S12），所以左端點屬於區間；右端點同理。M 的每個元素 x 滿足 min M≤x≤max M（S09、S10），所以 M⊆[l,u]。



S14 · implies操作前

\tfrac{1}{3}<\tfrac{1}{2}\ \ (1\cdot2<1\cdot3)

操作後

\tfrac12\notin[l,u]

條件：無

規則：interval_def · 依賴：S03, S13, interval_def

葉節點依據：interval_def + contradiction + order_basics

依 L_cross（p=1、q=3、r=1、s=2）：1·2=2<3=1·3，所以 1/3<1/2。若 1/2≤1/3，與 1/3≤1/2 合用反對稱性得 1/2=1/3，與 1/3≠1/2 矛盾；所以 1/2≤u 不成立，1/2 不在區間內。



S15 · equivalent操作前

-\tfrac{7}{12}<-\tfrac{5}{9}

操作後

-\tfrac{7}{12}+\tfrac{7}{12}<-\tfrac{5}{9}+\tfrac{7}{12},\ \text{i.e.}\ 0<\tfrac{1}{36}

條件：無

規則：L_translate · 依賴：S02, S04

葉節點依據：order_basics + frac_rules + numeric_evaluation

用 L_translate 取 c=7/12：−7/12<−5/9 ⇔ 0<−5/9+7/12。計算 −5/9+7/12=−20/36+21/36=1/36>0，與 S04 一致。平移不改變比較，所以它只是重寫，不是新的題型。



S16 · implies操作前

\text{S02 to S15}

操作後

\min M=-\tfrac{7}{12},\ \max M=\tfrac13,\ l,u\in[l,u],\ \tfrac12\notin[l,u]

條件：無

規則：and_intro_elim · 依賴：S02, S03, S08, S09, S10, S11, S13, S14

葉節點依據：and_intro_elim

整理：加法保序與正分母交叉比較已證；非空有限集合的最小元素存在且唯一；M 的次序為 −7/12<−5/9<−1/2<1/3，最小 −7/12、最大 1/3；閉區間 [−7/12,1/3] 含兩端點與 M 全部元素，不含 1/2。







## 局部子步與引理

S02.1 · implies操作前

a<b

操作後

a+c<b+c

條件：無

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics

（⇒）這正是順序公理「u<v ⇒ u+w<v+w」取 u=a、v=b、w=c。



S02.2 · implies操作前

a+c<b+c

操作後

(a+c)+(-c)<(b+c)+(-c),\ \text{i.e.}\ a<b

條件：無

規則：order_basics · 依賴：order_basics, add_inverse

葉節點依據：order_basics + add_assoc + add_inverse + add_zero

（⇐）對 a+c<b+c 再用同一公理，取 w=−c，得 (a+c)+(−c)<(b+c)+(−c)；化簡兩邊（結合律、c+(−c)=0、加 0 不變）得 a<b。S02.1 與 S02.2 合起來證得引理 L_translate。



S03.1 · implies操作前

q>0,\ s>0

操作後

qs>0,\ \tfrac{1}{qs}>0

條件：q>0; s>0

規則：order_basics · 依賴：order_basics, mul_inverse_nonzero

葉節點依據：order_basics + mul_zero + mul_inverse_nonzero + contradiction

把 0<q 兩邊乘以 s>0 得 0·s<q·s，即 qs>0。qs≠0，所以 1/(qs) 存在；若 1/(qs)<0，乘以 qs>0 得 1<0，矛盾，而 1/(qs)≠0（因 (1/(qs))·qs=1），故 1/(qs)>0。



S03.2 · implies操作前

\frac{p}{q}<\frac{r}{s}

操作後

\frac{p}{q}\cdot qs<\frac{r}{s}\cdot qs,\ \text{i.e.}\ ps<rq

條件：qs>0

規則：order_basics · 依賴：S03.1, frac_rules

葉節點依據：order_basics + frac_rules + mul_comm + mul_assoc

（⇒）兩邊乘以正數 qs，順序保持；化簡 (p/q)·qs=ps、(r/s)·qs=rq（分式規則，q、s≠0）。



S03.3 · implies操作前

ps<rq

操作後

\frac{ps}{qs}<\frac{rq}{qs},\ \text{i.e.}\ \frac{p}{q}<\frac{r}{s}

條件：\tfrac{1}{qs}>0

規則：order_basics · 依賴：S03.1, frac_rules

葉節點依據：order_basics + frac_rules

（⇐）兩邊乘以正數 1/(qs)（S03.1），順序保持；約分 ps/(qs)=p/q、rq/(qs)=r/s。S03.1 至 S03.3 合起來證得引理 L_cross。



S08.1 · induction_base操作前

M=\{a\}

操作後

\min M=a

條件：無

規則：nat_induction · 依賴：G3, min_max_def

葉節點依據：min_max_def + order_basics

基礎 n=1：M={a}。a∈M，且 M 唯一的元素 x=a 滿足 a≤a（自反），所以 a 是最小元素（也是最大元素）。



S08.2 · induction_step操作前

|M|=n+1,\ a\in M,\ m'=\min(M\setminus\{a\})

操作後

\min M=m'\ \text{if}\ m'\le a,\ \ \min M=a\ \text{if}\ a<m'

條件：n\ge1

規則：nat_induction · 依賴：S08.1, min_max_def, case_analysis

葉節點依據：nat_induction + case_analysis + order_basics + min_max_def

歸納步：設所有 n 個元素的非空集合都有最小元素（n≥1）。取 |M|=n+1 與 a∈M，M′=M∖{a} 有 n 個元素，依歸納假設有最小元素 m′。依三分律分兩種情形：若 m′≤a，則 m′ 不大於 M′ 的每個元素，也不大於 a，所以 m′ 是 M 的最小元素；若 a<m′，則對 x∈M′ 有 a<m′≤x，傳遞得 a≤x，又 a≤a，所以 a 是最小元素。S08.1 與 S08.2 合起來證得引理 L_finite_min。



S11.1 · implies操作前

m,m'\in M,\ m\le x,\ m'\le x\ \forall x\in M

操作後

m\le m',\ m'\le m\ \Rightarrow\ m=m'

條件：無

規則：mko_order · 依賴：min_max_def, G1

葉節點依據：min_max_def + mko_order

m 是最小元素且 m′∈M，所以 m≤m′；同理 m′≤m。依反對稱性 m=m′。最大元素以 ≥ 同樣證明。此步證得引理 L_min_unique。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S13, S14, and_intro_elim — 目標 G 為 goal 中的證明與判定；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。
- S15 · inverse_equivalence · L_translate, frac_rules, numeric_evaluation — L_translate 是等價，兩邊同加 7/12 或同減 7/12 互為反向。
- S14 · premise_audit · L_cross, interval_def, contradiction — 成員條件是兩個不等式的合取，否定其中一個就足以排除。
- S13 · premise_audit · interval_def, S12, mko_order — 端點屬於閉區間只用到自反性與 l≤u；開區間是另一個物件，不在此討論。
- S12 · premise_audit · S07, order_basics — 由 l<u 得 l≤u 是嚴格順序的定義。
- S11.1 · premise_audit · min_max_def, mko_order — 只用到兩個最小元素都屬於 M 以及反對稱性。
- S11 · premise_audit · L_min_unique — 唯一性依賴反對稱性。
- S10 · premise_audit · S07, min_max_def — 與 S09 對稱。
- S09 · premise_audit · S07, min_max_def, order_basics — 兩個條件（屬於 M、不大於每個元素）都已檢查；由 x<y 得 x≤y 是嚴格順序的定義。
- S08.2 · premise_audit · nat_induction, case_analysis, order_basics, min_max_def — 需要 n≥1 使 M′ 非空，歸納假設才適用；兩個情形由全序性窮盡。
- S08.1 · premise_audit · min_max_def, order_basics — 只用到自反性；單元素集合的兩個極值相同。
- S08 · premise_audit · L_finite_min — 非空是必要的：歸納從 n=1 開始，空集合不在範圍內，也沒有最小元素。
- S07 · premise_audit · S04, S05, S06, order_basics — 需要的是三個相鄰比較與傳遞性；不需要再做其餘三對的交叉相乘。
- S06 · inverse_equivalence · L_cross, numeric_evaluation — 同 S04，分母為正，等價成立。
- S05 · inverse_equivalence · L_cross, numeric_evaluation — 同 S04，分母為正，等價成立。
- S04 · inverse_equivalence · L_cross, numeric_evaluation — L_cross 是等價，條件 12、9>0 成立，所以分數比較與整數比較同真同假。
- S03.3 · premise_audit · S03.1, order_basics, frac_rules — 需要 1/(qs)>0，由 S03.1 提供。
- S03.2 · premise_audit · S03.1, order_basics, frac_rules — 需要 qs>0；若 qs<0，乘法會使不等號反向。
- S03.1 · premise_audit · order_basics, mul_inverse_nonzero, contradiction — 兩個正數的積為正，正數的倒數為正；兩者都依賴 q、s>0。
- S03 · inverse_equivalence · L_cross — ⇒ 與 ⇐ 分別在子步中證明，條件 q、s>0 兩個方向都要用。
- S02.2 · premise_audit · order_basics, add_assoc, add_inverse, add_zero — 每個實數 c 都有加法反元素 −c，所以這個方向不需附加條件。
- S02.1 · premise_audit · order_basics — 直接套用公理，對任何實數 c 成立。
- S02 · inverse_equivalence · L_translate — 兩個方向都有證明，所以是等價。
- S01 · premise_audit · G1, mko_order, order_basics — 只是定義與公理的重述；三分律在 order_basics 中也列為前提。





## 錯誤控制與反例

交叉相乘前分母須為正MKO 的誤解之一是忽略分母正負。比較 1/(−2) 與 1/3 時直接交叉相乘得 1·3=3>−2=1·(−2)，會誤判 1/(−2)>1/3；實際上 1/(−2)=−1/2<1/3。原因是乘上負數 (−2)·3 使不等號反向。先寫成正分母 (−1)/2 再比較：(−1)·3=−3<2，結論正確。

閉區間包含端點另一個誤解是漏掉閉區間的端點。l≤l≤u 成立，所以 l∈[l,u]（S13）。l=u 時 [l,u] 只含一個值，例如 [2,2]={2}；不含端點的是開區間，那是另一個物件。

極值看值不看次序，空集合沒有極值M 列出時 −5/9 在第一個，但最小元素是 −7/12（S09）。空集合沒有最小元素，因為不存在 m∈∅；S08 的歸納從 n=1 開始，不涵蓋空集合，不能替空集合指定任意極值。


- 1/(−2) 與 1/3 交叉相乘得 1·3=3>−2=1·(−2)，所以 1/(−2)>1/3 → reject — 分母 −2 為負，L_cross 不適用；1/(−2)=−1/2<1/3。
- −7/12 是端點，所以不屬於 [−7/12,1/3] → reject — −7/12≤−7/12≤1/3 成立，閉區間包含端點。
- M 的最小元素是 −5/9，因為它列在第一個 → reject — −7/12<−5/9（S04），最小元素由值決定，是 −7/12。
- 空集合的最小元素是 0 → reject — 最小元素必須屬於該集合，而 0∉∅；空集合沒有最小元素。





## 結論與限制

對所有實數 a、b、c，a<b ⇔ a+c<b+c；q、s>0 時 p/q<r/s ⇔ ps<rq；非空有限實數集合有唯一的最小元素（最大元素同理）。M 的元素排成 −7/12<−5/9<−1/2<1/3，所以 min M=−7/12、max M=1/3（與列出次序無關）；[−7/12,1/3] 是合法閉區間，包含兩端點與 M 的全部元素，不包含 1/2。


- 順序公理（order_basics）作為前提使用，本稿不從實數的構造推導它們。
- 最大元素的存在只以「同一論證把 ≤ 換成 ≥」說明，未逐步寫出。





## 驗證及來源綁定

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


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

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