圖匹配

數學敘述

完整有限無向簡單圖上核每條選邊存在及端點互斥。另分清matching、maximal、maximum與perfect；較大matching witness可否證maximum，但單一matching不給最優性。

代表公式（精確 TeX）

M(G)

成立條件

• 完整有限無向無loop簡單圖。
• matching以原圖edge indices選取並正規化。

符號作用域

• M — 匹配
• G — 有限簡單圖

直觀、定義與常見誤解

選取邊必須存在於原圖。

任兩選邊端點集合不交。

maximal是不可再加邊；maximum是全域最大基數；兩者不同。

把無法再加一邊當成全域最大，或把perfect與maximum混同。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 有限簡單無向圖 — 提供完整頂點與邊。
• 子集合 — matching為邊集合的子集。

驗證界線

只核完整有限圖及供給witness；沒有全域證書時不宣稱maximum。

not_formalized

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

下一個義務

加入maximum matching與Hall定理。

同源結構化資料

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