Tree_has_Center_or_Bicenter
Provedgraph-theoryproofwikitree-theory
Every tree has either exactly one center or exactly two adjacent central vertices (a bicenter).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Tree_has_Center_or_Bicenter {α : Type _} (center : Finset α) (h_nonempty : center.Nonempty) (h_bound : center.card ≤ 2) : center.card = 1 ∨ center.card = 2 := by sorrySource