English
If G is a tree, then the number of edges is exactly the number of vertices minus one.
Русский
Для дерева число рёбер равно числу вершин минус один.
LaTeX
$$$G.IsTree \Rightarrow \operatorname{card}(G.edgeFinset) + 1 = \operatorname{card}(V)$$$
Lean4
theorem card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
Finset.card G.edgeFinset + 1 = Fintype.card V :=
by
have := hG.isConnected.nonempty
inhabit V
classical
have : Finset.card ({ default } : Finset V)ᶜ + 1 = Fintype.card V := by
rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
rw [← this, add_left_inj]
choose f hf hf' using (hG.existsUnique_path · default)
refine Eq.symm <| Finset.card_bij (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj
case notNil => exact not_nil_of_ne (by simpa using hw)
case memEdges => simp
case inj =>
intro a ha b hb h
wlog h' : (f a).length ≤ (f b).length generalizing a b
· exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
rw [dart_edge_eq_iff] at h
obtain (h | h) := h
· exact (congrArg (·.fst) h)
· have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
· rw [length_copy, ← add_left_inj 1, length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
cutsat
· simp only [isPath_copy]
exact (hf _).tail
case surj =>
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
intro x y h
wlog h' : (f x).length ≤ (f y).length generalizing x y
· rw [Sym2.eq_swap]
exact this y x h.symm (le_of_not_ge h')
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
· rintro rfl
rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
length_cons, length_nil] at h'
simp at h'
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
· simp only [firstDart_toProd, getVert_cons_succ, getVert_zero, Prod.swap_prod_mk]
case
contra =>
suffices (f x).takeUntil y hy = .cons h .nil
by
rw [← take_spec _ hy] at h'
simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
simp [h.ne]
