English
For a tree, the edgeFinset has a cardinality related to the vertex set; more precisely, card(edgeFinset) + 1 = card(V).
Русский
Для дерева выполняется равенство, связывающее количество рёбер и вершин: card(edgeFinset) + 1 = card(V).
LaTeX
$$$IsTree(G) \Rightarrow \operatorname{card}(G.edgeFinset) + 1 = \operatorname{card}(V)$$$
Lean4
/-- The minimum degree of all vertices in a nontrivial tree is one. -/
theorem minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [Nontrivial V] [DecidableRel G.Adj] :
G.minDegree = 1 := by
by_cases q : 2 ≤ G.minDegree
· have := h.card_edgeFinset
have := G.sum_degrees_eq_twice_card_edges
have hle : ∑ v : V, 2 ≤ ∑ v, G.degree v := by
gcongr
exact le_trans q (G.minDegree_le_degree _)
rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle
cutsat
· have := h.isConnected.preconnected.minDegree_pos_of_nontrivial
cutsat
