Nontrivial trees have minimum degree one

Stream: Is there code for X?

[Laurance Lau]

I couldn't find code for this.

lemma Preconnected.degree_pos_of_nontrivial [Nontrivial V] {G : SimpleGraph V} (h : G.Preconnected)
    (v : V) [Fintype (G.neighborSet v)] : 0 < G.degree v := by
  simp [degree_pos_iff_mem_support, h.support_eq_univ]

lemma Preconnected.minDegree_pos_of_nontrivial [Nontrivial V] [Fintype V] {G : SimpleGraph V}
    [DecidableRel G.Adj] (h : G.Preconnected) : 0 < G.minDegree := by
  rw [G.exists_minimal_degree_vertex.choose_spec]
  exact h.degree_pos_of_nontrivial G.exists_minimal_degree_vertex.choose

/-- The minimum degree of all vertices in a nontrivial tree is one. -/
lemma IsTree.minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [inst : Nontrivial V]
    [DecidableRel G.Adj] : G.minDegree = 1 := by
  by_cases q : 2 ≤ G.minDegree
  · have := Fintype.one_lt_card_iff_nontrivial.mpr inst
    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 _)
    simp at hle
    omega
  · linarith [h.isConnected.preconnected.minDegree_pos_of_nontrivial]

/-- A nontrivial tree has a vertex of degree one. -/
lemma IsTree.exists_vert_degree_one_of_nontrivial [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
    (h : G.IsTree) : ∃ v, G.degree v = 1 := by
  bound [G.exists_minimal_degree_vertex, h.minDegree_eq_one_of_nontrivial]

[Laurance Lau]

Oh, it seems this has been attempted before... #graph theory > connectivity @ 💬