card_vert_le_card_edgeSet_add_one

English

In a connected graph, the number of vertices is at most the number of edges plus one.

Русский

В связном графе число вершин не превышает число рёбер плюс единица.

LaTeX

$$$G.Connected \Rightarrow \operatorname{card}(V) \le \operatorname{card}(G.edgeSet) + 1$$$

Lean4

/-- Every connected graph on `n` vertices has at least `n-1` edges. -/
theorem card_vert_le_card_edgeSet_add_one (h : G.Connected) : Nat.card V ≤ Nat.card G.edgeSet + 1 :=
  by
  obtain hV | hV := (finite_or_infinite V).symm
  · simp
  have := Fintype.ofFinite
  obtain ⟨T, hle, hT⟩ := h.exists_isTree_le
  rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, add_le_add_iff_right, Nat.card_eq_fintype_card, ← edgeFinset_card]
  exact Finset.card_mono <| by simpa

Похожие утверждения