跳轉到

10.2 圖論入門#

本節目標#

  • 建立圖的直覺，理解 SimpleGraph 的形式定義。
  • 熟悉 Mathlib 中 SimpleGraph 的基本操作：鄰接 adj、鄰居集合 neighborSet。
  • 定義並使用度數（degree），證明握手引理。
  • 認識 Euler 路徑存在條件（敘述層級）。
  • 計算完全圖 \(K_n\) 的邊數，認識樹的基本性質。

圖的直覺與定義#

圖（graph）描述「物件與物件之間的關係」：頂點（vertex）是物件， 邊（edge）是關係。例如社交網路中，人是頂點，「相識」是邊。

定義（簡單圖）：簡單圖由頂點集 \(V\) 與邊集 \(E \subseteq \binom{V}{2}\) 組成，其中 \(\binom{V}{2}\) 表示 \(V\) 的所有二元子集。特點： - 沒有自環（邊不連接頂點到自己）； - 任兩點之間至多一條邊； - 邊無方向。

Mathlib 的 SimpleGraph 把「邊集」表示成一個對稱、無自環的二元關係：

#check @SimpleGraph
-- structure SimpleGraph (V : Type*) where
--   Adj : V → V → Prop
--   symm : ∀ a b, Adj a b → Adj b a
--   loopless : ∀ a, ¬ Adj a a

也就是說，SimpleGraph V 是「 \(V\) 上的對稱無自環關係」的全體。 兩個頂點相鄰寫作 G.Adj a b。

鄰接與鄰居集合#

基本操作：

open SimpleGraph

-- 完全圖 Kₙ：任何兩個不同頂點都相鄰
#check @SimpleGraph.completeGraph

-- 邊的定義：對簡單圖而言，一條邊就是一對相鄰頂點
#check @SimpleGraph.edgeSet

-- 鄰居集合：a 的所有鄰居
#check @SimpleGraph.neighborSet
-- SimpleGraph.neighborSet (G : SimpleGraph V) (a : V) : Finset V

neighborSet 在 Mathlib 中是一個 Finset（頂點集可枚舉時）， 我們可以問「某點有幾個鄰居」：

example (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (a : V) :
    G.neighborSet a.card = G.degree a := rfl

度數的定義即鄰居個數： \(\deg(a) = \left|N(a)\right|\) 。

#check @SimpleGraph.degree
-- SimpleGraph.degree (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (a : V) : ℕ

握手引理#

定理（握手引理，handshake lemma）：

\[ \sum_{v \in V} \deg(v) = 2 \left|E\right|。 \]

證明正是「算兩次」（見 10.1 節）：把「邊的端點」這個集合按頂點分類 得到度數總和，按邊分類得到每條邊貢獻 \(2\) 。

在 Mathlib 中，與度數和有關的引理可由 SimpleGraph 的度數定義 出發證明。以下示範以 Finset.sum 表達握手引理的骨架：

example (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] :
    ∑ v, G.degree v = 2 * G.edgeFinset.card := by
  -- 思路：degree v = neighborSet v 的 card，
  -- 對所有 v 求和即是「所有有序鄰接對 (a, b)」的數量，
  -- 而每條邊恰產生兩個有序對 (a, b) 與 (b, a)。
  sorry -- 完整證明見練習

骨架思路（供填洞）：

  1. 每條邊 \(\{a, b\}\) 貢獻兩個有序對 \((a,b)\) 與 \((b,a)\) ，這用到 G.symm（對稱性）。
  2. 固定 \(a\) ，滿足 G.Adj a b 的有序對個數就是 G.degree a。
  3. 在 Mathlib 中可搜尋 Finset.sum_biUnion、Finset.card_union_of_disjoint 等計數工具，或搜尋 SimpleGraph 命名空間下含 degree 的引理。

Euler 路徑#

定義：一條 Euler 路徑是「每條邊恰好經過一次」的路徑；若它起點與 終點相同，稱為 Euler 迴路。

定理（Euler，敘述層級）：連通圖存在 Euler 迴路，若且唯若每個頂點 的度數都是偶數。存在（不必閉合的）Euler 路徑，若且唯若度數為奇數的 頂點恰有 \(0\) 或 \(2\) 個。

必要方向的直覺：路徑每「進入再離開」一個頂點消耗兩個度數， 所以中間頂點的度數必為偶數；只有起終點允許奇度數。

在 Mathlib 中，Euler 型的結果與 SimpleGraph.walk 與 SimpleGraph.IsEulerian 相關，可直接查閱：

#check @SimpleGraph.IsEulerian
-- 一個常見的入口：Mathlib 已證「度數全偶 + 連通 → 存在 Euler 迴路」
-- 相關引理位於 SimpleGraph 命名空間，關鍵字：IsEulerian

本書以敘述層級理解即可；完整形式化涉及構造性證明（逐步拆解迴路）， 屬進階題材。

範例：完全圖 \(K_n\) 的邊數#

完全圖 \(K_n\) ：任兩相異頂點都相鄰。顯然

\[ \left|E(K_n)\right| = \binom{n}{2} = \frac{n(n-1)}{2}。 \]

這又是一個算兩次：按頂點數 \(n\) 算，每個頂點有 \(n-1\) 個鄰居， 度數總和 \(n(n-1)\) ；每條邊被算了兩次，故除以 \(2\) 。而 \(\binom{n}{2}\) 恰是「從 \(n\) 點選兩點當邊」的計數——與 10.1 節的 組合數呼應。

在 Lean 中，可對具體的 \(n\) （如 \(n = 4\) ）用 decide 或計算驗證：

-- K₄ 有 6 條邊 = C(4,2)
example : Nat.choose 4 2 = 6 := by decide

一般情形的完整形式化需要把 completeGraph 的 edgeFinset.card 算出來，適合作為練習挑戰。

樹的基本性質#

定義：樹（tree）是連通且無圈的圖。

樹的三條經典性質（互相等價）：

  1. \(n\) 個頂點的樹恰有 \(n - 1\) 條邊。
  2. 任兩頂點之間有唯一的簡單路徑。
  3. 樹去掉任一條邊就不連通（邊都是「橋」）。

性質 1 的直覺：從單點開始（ \(0\) 條邊），每加入一個新頂點恰好 加入一條邊維持連通且無圈。

在 Mathlib 中，樹相關概念可用 SimpleGraph.IsTree（或以連通 + 無圈的組合表達）：

#check @SimpleGraph.IsTree
#check @SimpleGraph.Connected
#check @SimpleGraph.IsAcyclic

性質 2（唯一路徑）在 Mathlib 中有對應敘述，關鍵字含 unique 與 path；這些是練習 4 的探索方向。

小結與練習#

本節重點：

  • SimpleGraph V = \(V\) 上的對稱無自環關係；G.Adj a b 表相鄰。
  • G.degree a = (G.neighborSet a).card。
  • 握手引理 \(\sum_v \deg(v) = 2|E|\) 是「算兩次」的經典應用。
  • Euler 迴路存在 ⟺ 連通且所有度數為偶（敘述層級）。
  • \(|E(K_n)| = \binom{n}{2}\) ；樹：連通 + 無圈， \(n\) 頂點 \(n-1\) 邊。

練習：

  1. 證明： \(\sum_v \deg(v)\) 總是偶數（不必先算出 \(|E|\) ；提示：把度數和 按「與 \(a\) 相鄰的有序對」重排，利用 G.symm 配對）。
  2. 證明：度數為奇數的頂點個數必為偶數（握手引理的直接推論）。
  3. 計算 \(K_5\) 的邊數與每個頂點的度數，用 Nat.choose 表達並以 decide 驗證。
  4. 探索題：在 Mathlib 中搜尋樹的「唯一路徑」性質的引理名稱與敘述， 抄下其 Lean 陳述並逐詞解讀。
  5. 挑戰：對 \(n = 3\) 的完全圖 \(K_3\) ，把 completeGraph 的 edgeFinset 展開檢查恰有 3 條邊。