# 凸集合

集合凸表示任兩點及每個lambda∈[0,1]形成的整條線段仍在集合內。

mko-convex-set · definition · v0.10.0



## 數學敘述

實向量空間子集C為凸，若對所有x,y∈C及所有lambda∈[0,1]，lambda x+(1-lambda)y仍屬C。本輪正例只用區間、盒與半空間的完整代數證書；單一精確反例可否證凸性。





## 代表公式（精確 TeX）

K(C)





## 成立條件


- 只處理非空閉區間、非空軸對齊盒、閉半空間與明示有限點集反例。
- 有限lambda抽樣不能證凸；有限點集反例失敗也不能反向證明該集合凸。





## 符號作用域


- K — 凸性證書或反例
- C — 實向量空間子集





## 直觀、定義與常見誤解

區間與盒由逐座標上下界證書處理所有lambda。

半空間由線性不等式對凸組合封閉。

若集合含兩端點卻不含其中點，一個midpoint witness即足以否證。

檢查幾個lambda就宣稱凸，或找不到一個反例便宣稱凸。





## 已採用的推導導讀

[凸集合：半空間與軸對齊盒的完整凸性證書，及有限點集的中點反例](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-convex-set-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有限凸組合](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-convex-combination/) — 兩點凸組合描述線段。
- [子集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) — 凸集合是實向量空間的子集。
- [實向量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-vector-space/) — 線段運算依賴向量加法與純量乘法。





## 驗證界線

正例需全稱代數證書；反例失敗不構成正證明。

not_formalized

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





## 下一個義務

加入凸函數、凸包與凸最佳化。





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/convex-set.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-convex-set/index.md)