# 非空有限樹：連通、無環與唯一道路

非空有限簡單無向圖同時連通且無環才是樹；保留單點、度1葉及加一條新邊的唯一環。

mko-tree · concept · v0.10.0



## 數學敘述

在有限簡單無向圖G=(V,E)中，本條目約定樹為V非空、任意兩頂點可由道路連接，且沒有簡單環的圖。道路不重複頂點；同一頂點到自身的零邊道路合法。樹中任意兩頂點有唯一道路；葉定義為度數恰1的頂點。





## 代表公式（精確 TeX）

T(V,E)





## 成立條件


- 題庫V至多10個相異安全整數標籤，E的每項恰兩個V中相异頂點；無向邊方向與重複列項正規化。自環、缺失端點及多重圖語義不在切片。
- 空圖不是樹；單點無邊圖是樹，但其頂點度0，因此本葉慣例下葉集為空。
- 加邊題先要求原圖是樹，u、v在V中相異且原邊不存在。新增這條邊與原唯一道路形成唯一簡單環；已存在邊不適用。





## 符號作用域


- T — 非空有限樹資格
- V — 互異頂點集合
- E — 簡單無向邊集合





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

僅有|E|=|V|−1不足以判樹，還需連通；一個三角形加孤點具有這個邊數卻不是樹。空圖與單点的處理明示，不借用模糊的圖形直覺。

唯一道路以實際頂點順序輸出，不列排序後的集合。加新邊的環從兩端較小標籤出發，沿原道路到較大標籤，再以新增邊回起點。葉按度1列遞增集合；一般樹定理仍須形式證明。

只看邊數就判樹、將單點度0叫度1葉，或把已有邊重列當成新增環。





## 已採用的推導導讀

[樹：判定一個 6 頂點圖是樹，求葉、唯一道路與加邊後的唯一環](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-tree-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有限簡單無向圖](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph/) — 固定無自環、無重邊與無向邊集合語義。





## 驗證界線

有限圖切片可完全重算；樹的普遍等價定理及形式Evidence尚未建立。

not_formalized

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





## 下一個義務

固定Mathlib SimpleGraph.IsTree的Connected非空條件，綁定唯一道路、度1葉與非相鄰加邊環。





## 同源結構化資料

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

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