# 凸集合：半空間與軸對齊盒的完整凸性證書，及有限點集的中點反例 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-convex-set/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-convex-set-01 · production-20261019-adopted-96 ## 目標與範圍在實向量空間 ℝ² 中：（一）證明閉半空間 H={(x,y) ∣ 2x−3y≤6} 是凸集合；（二）證明非空軸對齊盒 B=[−1,2]×[0,3] 是凸集合；兩個證明都必須對所有 p、q 與所有 λ∈[0,1] 成立。（三）用一個精確的中點見證否證有限點集 F={(0,0),(2,0),(0,2)} 的凸性，並說明為何抽查有限個 λ、或找不到反例，都不能證明凸性。停在 MKO 的切片內：閉半空間、非空軸對齊盒（逐座標區間）與明示有限點集的反例。正面結論都用對所有 p、q、λ 成立的代數證書；不使用拓撲、凸包或分離定理；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - order_basics - distributive - mul_zero - forall_intro - quantifier_negation - cartesian_product_def - G1 — ℝ² 是實向量空間，加法與純量乘法逐座標進行：(a,b)+(c,d)=(a+c,b+d)，t(a,b)=(ta,tb)。 - G2 — H={(x,y)∈ℝ² ∣ 2x−3y≤6}，法向量 (2,−3)≠(0,0) 的閉半空間。 - G3 — B=[−1,2]×[0,3]={(x,y) ∣ −1≤x≤2 且 0≤y≤3}，非空軸對齊盒。 - G4 — F={(0,0),(2,0),(0,2)}，恰有這三個元素的明示有限點集。 - H — 閉半空間 2x−3y≤6 - B=[-1,2]\times[0,3] — 軸對齊盒 - F — 三點的有限集合 - p=(x_1,y_1),\ q=(x_2,y_2) — 任取的兩點 - \lambda\in[0,1] — 凸組合的權重 - z=\lambda p+(1-\lambda)q — p 與 q 的凸組合 ## 規則與來源 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - add_zero · prerequisite — 加法單位元：u+0=u。 - mko_convex · cited — 實向量空間的子集 C 為凸，若對所有 x,y∈C 及所有 λ∈[0,1]，λx+(1−λ)y 仍屬於 C。正例用區間、盒與半空間的完整代數證書；單一精確反例可否證凸性。 · mko-convex-set - coord_ops · prerequisite — 逐座標運算：(a,b)+(c,d)=(a+c,b+d)，t(a,b)=(ta,tb)。 - ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂。 - L_mono · lemma — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv。 - L_interval · lemma — 區間的凸性證書：若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β。 ## 逐步主鏈 S01 · equivalent操作前 H\ \text{convex} 操作後 \forall p,q\in H\ \forall\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\in H 條件：無規則：mko_convex · 依賴：G2, mko_convex 葉節點依據：mko_convex + def_unfold 依 MKO 的定義展開「H 是凸的」：對 H 中所有點 p、q 與 [0,1] 中所有 λ，凸組合仍在 H 中。這是一個對三個變數的全稱命題，證明必須覆蓋所有情況，不能只檢查幾個 λ。 S02 · equivalent操作前 p=(x_1,y_1)\in H,\ q=(x_2,y_2)\in H,\ \lambda\in[0,1] 操作後 2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6,\ 0\le\lambda\le 1 條件：無規則：set_builder · 依賴：S01, G2, set_builder 葉節點依據：set_builder + def_unfold 任取 H 中的 p、q 與 [0,1] 中的 λ，除此之外不加任何假設（以便最後做 ∀ 引入）。依集合建構式，p∈H 就是 2x₁−3y₁≤6，q∈H 就是 2x₂−3y₂≤6；λ∈[0,1] 就是 0≤λ≤1。 S03 · equivalent操作前 z=\lambda p+(1-\lambda)q 操作後 z=(\lambda x_1+(1-\lambda)x_2,\ \lambda y_1+(1-\lambda)y_2) 條件：無規則：coord_ops · 依賴：G1, S02, coord_ops 葉節點依據：coord_ops + eq_replace 依 G1 的逐座標運算：λp=(λx₁,λy₁)，(1−λ)q=((1−λ)x₂,(1−λ)y₂)，相加即得 z 的兩個座標。 S04 · equivalent操作前 2z_1-3z_2 操作後 \lambda(2x_1-3y_1)+(1-\lambda)(2x_2-3y_2) 條件：無規則：distributive · 依賴：S03 葉節點依據：distributive + mul_comm + add_comm + add_assoc 把 z₁=λx₁+(1−λ)x₂、z₂=λy₁+(1−λ)y₂ 代入 2z₁−3z₂，展開後按 λ 與 1−λ 重新分組：2λx₁+2(1−λ)x₂−3λy₁−3(1−λ)y₂=λ(2x₁−3y₁)+(1−λ)(2x₂−3y₂)。這說明線性式在凸組合上等於兩端值的同權重組合（N1 是這個多項式恆等式的核對）。 S05 · implies操作前 0\le\lambda\le 1 操作後 \lambda\ge 0,\ 1-\lambda\ge 0 條件：無規則：order_basics · 依賴：S02, order_basics 葉節點依據：order_basics λ≥0 直接來自 S02。由 λ≤1，兩邊同加 −λ 得 0≤1−λ。兩個權重都非負，下一步乘不等式時方向不變就靠這一點。 S06 · implies操作前 2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6 操作後 \lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda) 條件：\lambda\ge 0; 1-\lambda\ge 0 規則：L_mono · 依賴：S02, S05, L_mono 葉節點依據：L_mono 用引理 L_mono 兩次：第一式乘以 w=λ≥0，第二式乘以 w=1−λ≥0，不等號方向不變。引理在 S06.1、S06.2 中分 w>0 與 w=0 兩種情況證明。 S07 · implies操作前 \lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda) 操作後 2z_1-3z_2\le 6\lambda+6(1-\lambda)=6 條件：無規則：ineq_add · 依賴：S04, S06, ineq_add 葉節點依據：ineq_add + distributive + eq_replace 兩個不等式相加，左邊依 S04 正是 2z₁−3z₂；右邊依分配律 6λ+6(1−λ)=6(λ+1−λ)=6。所以 2z₁−3z₂≤6。 S08 · implies操作前 2z_1-3z_2\le 6 操作後 z\in H\ \text{for all } p,q\in H,\ \lambda\in[0,1];\ H\ \text{convex} 條件：無規則：forall_intro · 依賴：S07, S01, S02, forall_intro 葉節點依據：forall_intro + set_builder 依集合建構式，2z₁−3z₂≤6 表示 z∈H。p、q、λ 在 S02 中是任取的，沒有任何額外假設，所以依 ∀ 引入，S01 的全稱命題成立：H 是凸集合。這是覆蓋所有 λ∈[0,1] 的完整證書，而不是抽樣。 S09 · equivalent操作前 B\ \text{convex} 操作後 \forall p,q\in B\ \forall\lambda\in[0,1]:\ -1\le z_1\le 2\ \land\ 0\le z_2\le 3 條件：無規則：cartesian_product_def · 依賴：G3, S03, mko_convex, cartesian_product_def 葉節點依據：cartesian_product_def + def_unfold 依定義展開 B 的凸性，並用 B=[−1,2]×[0,3]：z∈B 等價於第一座標在 [−1,2]、第二座標在 [0,3]。依 S03（同樣的逐座標計算），z₁=λx₁+(1−λ)x₂、z₂=λy₁+(1−λ)y₂，而 p、q∈B 給出 −1≤x₁,x₂≤2 與 0≤y₁,y₂≤3。盒的條件逐座標分開，所以只需對每個座標證明區間條件。 S10 · implies操作前 -1\le x_1,x_2\le 2,\ 0\le y_1,y_2\le 3,\ \lambda\in[0,1] 操作後 -1\le z_1\le 2,\ 0\le z_2\le 3 條件：\lambda\in[0,1] 規則：L_interval · 依賴：S09, L_interval 葉節點依據：L_interval 對第一座標用引理 L_interval（α=−1、β=2、s=x₁、t=x₂），對第二座標用同一引理（α=0、β=3、s=y₁、t=y₂）。引理在 S10.1 至 S10.3 中對任意 α≤β 證明，所以一次涵蓋所有 λ∈[0,1]。 S11 · implies操作前 -1\le z_1\le 2,\ 0\le z_2\le 3 操作後 z\in B\ \text{for all } p,q\in B,\ \lambda\in[0,1];\ B\ \text{convex} 條件：無規則：forall_intro · 依賴：S10, S09, forall_intro 葉節點依據：forall_intro + and_intro_elim 兩個座標條件合起來，依 S09 的等價就是 z∈B。p、q、λ 是任取的，依 ∀ 引入，B 是凸集合。這正是 MKO 所說盒由逐座標上下界證書處理所有 λ。 S12 · equivalent操作前 \neg(F\ \text{convex}) 操作後 \exists p,q\in F\ \exists\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\notin F 條件：無規則：quantifier_negation · 依賴：G4, mko_convex, quantifier_negation 葉節點依據：quantifier_negation + def_unfold 否定凸性的定義：¬∀ 等價於 ∃¬。所以要否證 F 的凸性，只需找到一組 p、q∈F 與 λ∈[0,1]，使凸組合不在 F 中。 S13 · equivalent操作前 p=(0,0),\ q=(2,0),\ \lambda=\tfrac12 操作後 \tfrac12 p+\tfrac12 q=(1,0) 條件：無規則：coord_ops · 依賴：G1, G4, coord_ops 葉節點依據：coord_ops + numeric_evaluation 取 F 中的 p=(0,0)、q=(2,0) 與 λ=1/2∈[0,1]。逐座標計算：(1/2)·0+(1/2)·2=1，(1/2)·0+(1/2)·0=0，所以中點是 (1,0)。 S14 · implies操作前 (1,0)\ \text{vs.}\ (0,0),(2,0),(0,2) 操作後 (1,0)\notin F 條件：無規則：cartesian_product_def · 依賴：S13, G4, cartesian_product_def 葉節點依據：cartesian_product_def + numeric_evaluation F 恰有三個元素。有序對相等需兩座標都相等：(1,0) 與 (0,0)、(2,0)、(0,2) 的第一座標分別是 1 對 0、1 對 2、1 對 0，都不相等。所以 (1,0) 不等於 F 的任何元素，(1,0)∉F。 S15 · implies操作前 p=(0,0),\ q=(2,0)\in F,\ \lambda=\tfrac12,\ (1,0)\notin F 操作後 F\ \text{is not convex} 條件：無規則：exists_intro · 依賴：S12, S13, S14, exists_intro 葉節點依據：exists_intro + quantifier_negation S13、S14 給出具體的 p、q、λ 使凸組合不在 F 中；依 ∃ 引入，S12 的存在命題成立，所以 F 不是凸集合。一個精確反例就足以否證（MKO para2）。 S16 · implies操作前 \lambda\in\{0,1\} 操作後 1\cdot p+0\cdot q=p\in F,\ 0\cdot p+1\cdot q=q\in F 條件：無規則：mul_zero · 依賴：S15, G1, mul_zero 葉節點依據：mul_zero + mul_one + add_zero 對任何集合與其中任何 p、q，λ=1 給出 p、λ=0 給出 q，都在集合內。所以 F 通過所有 λ∈{0,1} 的抽查，但 S15 已證 F 不凸。由此可見：只抽查有限個 λ（例如端點）通過，不能推出凸性；正面結論需要 S02 至 S08 那樣覆蓋所有 λ 的證書。 ## 局部子步與引理 S06.1 · implies操作前 u\le v,\ w>0 操作後 wu\le wv 條件：w>0 規則：order_basics · 依賴：order_basics, eq_congruence 葉節點依據：order_basics + eq_congruence + case_analysis u≤v 表示 u0，實數的序給出 wu0（S06.1）與 w=0（本步）兩種可能，分情況論證完成。S06.1 與 S06.2 合起來證得引理 L_mono。 S10.1 · implies操作前 \alpha\le s,\ \alpha\le t 操作後 \lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t 條件：\lambda\ge 0; 1-\lambda\ge 0 規則：L_mono · 依賴：L_mono, ineq_add, S05 葉節點依據：L_mono + ineq_add 依 L_mono（已在 S06.1、S06.2 證明），α≤s 乘以 λ≥0 得 λα≤λs；α≤t 乘以 1−λ≥0 得 (1−λ)α≤(1−λ)t（權重非負同 S05）。兩式相加得下界。 S10.2 · equivalent操作前 \lambda\alpha+(1-\lambda)\alpha 操作後 \alpha 條件：無規則：distributive · 依賴：S10.1, distributive 葉節點依據：distributive + mul_one + add_inverse 依分配律 λα+(1−λ)α=(λ+1−λ)α=1·α=α。代回 S10.1 得 α≤λs+(1−λ)t。 S10.3 · implies操作前 s\le\beta,\ t\le\beta 操作後 \lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta 條件：\lambda\ge 0; 1-\lambda\ge 0 規則：L_mono · 依賴：S10.1, S10.2, L_mono, ineq_add 葉節點依據：L_mono + ineq_add + distributive 上界同理：s≤β 乘以 λ、t≤β 乘以 1−λ，相加，再用 S10.2 的同一計算（把 α 換成 β）得 β。S10.1 至 S10.3 合起來證得引理 L_interval。 ## 逐步反向審查 - S16 · premise_audit · S15, mul_zero, mul_one — 只用乘以 0 與乘以 1 的性質及 S15。結論是「抽查通過不足以證凸」，由 F 這個具體反例支持；不宣稱任何抽查都會通過。 - S15 · premise_audit · S12, S13, S14, exists_intro — 需要見證中的 p、q 確實屬於 F、λ 確實在 [0,1]，且結果確實不在 F；三者都已核對。 - S14 · premise_audit · G4, cartesian_product_def — 需要 F 的完整列舉（G4 明示只有三點）；若 F 只是「至少含」這三點，此步不成立。 - S13 · inverse_equivalence · coord_ops, numeric_evaluation — 精確的有理數計算，兩邊是同一個點。 - S12 · inverse_equivalence · quantifier_negation, mko_convex — 量詞否定是雙向等價。 - S11 · premise_audit · S09, S10, forall_intro — 需要兩個座標的結論與 p、q、λ 的任意性。 - S10.3 · premise_audit · L_mono, ineq_add, distributive — 與 S10.1 對稱，只用 L_mono、不等式相加與分配律；沒有用 L_interval 本身。 - S10.2 · inverse_equivalence · distributive, mul_one — 反向：α=1·α=(λ+(1−λ))α=λα+(1−λ)α，對所有 λ 成立。 - S10.1 · premise_audit · L_mono, ineq_add, S05 — 本步證明引理 L_interval 的一部分，只用 L_mono 與不等式相加，沒有用 L_interval 本身。 - S10 · premise_audit · S09, L_interval — 需要兩端點都在區間內與 λ∈[0,1]。不宣稱反向：z 在區間內不推出 p、q 都在區間內。 - S09 · inverse_equivalence · cartesian_product_def, mko_convex, G3 — 屬於笛卡兒積等價於每個座標各自屬於對應區間，雙向成立。 - S08 · premise_audit · S07, S02, set_builder, forall_intro — ∀ 引入要求 p、q、λ 任意；S02 至 S07 沒有用到它們的具體值，條件成立。 - S07 · premise_audit · S04, S06, ineq_add, distributive — 需要兩個同向不等式與 S04 的恆等式。相加不可逆：由和的不等式不能推回各自的不等式，所以不宣稱反向。 - S06.2 · premise_audit · S06.1, mul_zero, case_analysis — 兩個情況涵蓋 w≥0 的全部可能；w<0 不在引理範圍內，且那時不等號會反向。 - S06.1 · premise_audit · order_basics, eq_congruence, case_analysis — 需要 w>0；u6，離開了 H。所以定義中的 λ∈[0,1] 不能省略。 - 對 F 中所有 p、q，λ=0 與 λ=1 的凸組合都在 F 中，所以 F 是凸的 → reject — 端點抽查對任何集合都通過；λ=1/2 時 (0,0) 與 (2,0) 的中點 (1,0)∉F。 - 嘗試 p=q=(0,0)、λ=1/2 沒有得到 F 外的點，所以 F 是凸的 → reject — 一個見證失敗不證明凸性；另一個見證 (0,0)、(2,0)、λ=1/2 成功否證。 - 對所有實數 λ（不限於 [0,1]），H 都對 λp+(1−λ)q 封閉 → reject — p=(3,0)、q=(0,0)、λ=2 給出 (6,0)，2·6−3·0=12>6。 - B 的凸性必須對每個有理數 λ 分別檢查才算證明 → reject — L_interval 對任意實數 λ∈[0,1] 一次證明，不需要也不能靠逐一檢查（λ 有無限多個）。 ## 結論與限制閉半空間 H={2x−3y≤6} 與盒 B=[−1,2]×[0,3] 都是凸集合：證明對所有 p、q 與所有 λ∈[0,1] 成立（線性式在凸組合上等於同權重組合，再乘以非負權重相加；盒逐座標用區間證書）。有限點集 F={(0,0),(2,0),(0,2)} 不是凸集合：(0,0) 與 (2,0) 的中點 (1,0) 不在 F 中。 - N6 至 N8、N10、N11 是 S07 的一個具體實例（p=(3,0)、q=(0,−2)、λ=1/3，z=(1,−4/3)），只作示範，證明不依賴它們。 - ineq_add 與 coord_ops 是本稿的前提，不在本稿中由實數公理推出。 ## 驗證及來源綁定 11 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f - original source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-convex-set-01.json)