English
For finite vertex sets, a graph is a tree iff it is connected and has exactly n − 1 edges, where n is the number of vertices.
Русский
Для конечного множества вершин граф является деревом тогда и только тогда, когда он связан и имеет ровно n − 1 рёбро, где n — число вершин.
LaTeX
$$$[Finite\ V] : IsTree(G) \iff (G.Connected \land \operatorname{card}(G.edgeSet) + 1 = \operatorname{card}(V))$$$
Lean4
theorem isTree_iff_connected_and_card [Finite V] : G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V :=
by
have := Fintype.ofFinite V
classical
refine ⟨fun h ↦ ⟨h.isConnected, by simpa using h.card_edgeFinset⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
simp_rw [isAcyclic_iff_forall_adj_isBridge]
refine fun x y h ↦
by_contra fun hbr ↦ (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card, ← edgeFinset_card,
add_lt_add_iff_right]
exact Finset.card_lt_card <| by simpa [deleteEdges]
