Theorems · Theorem · combinatorics

SimpleGraph.IsTree.exists_ne_and_degree_eq_one

∀ {V : Type u_1} {G : SimpleGraph V} [Nontrivial V] [Finite ↑G.edgeSet] [inst : G.LocallyFinite],
  G.IsTree → ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

A nontrivial finite tree has at least two leaves.

Defined in

Mathlib.Combinatorics.SimpleGraph.Acyclic

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontrivialFiniteSimpleGraph.LocallyFinite