theorem WrittenOnTheWallII.GraphConjecture5.conjecture5 {V : Type u_1} [Fintype V] [DecidableEq V] [Nontrivial V] (G : SimpleGraph V) (h_conn : G.Connected) : sSup ((fun (v : V) => ↑{w : V | w ∈ (fun (v : V) => {w : V | G.dist v w = G.radius.toNat}) v}.card) '' {v : V | G.eccent v = G.radius}) ≤ G.Ls

WOWII Conjecture 5

For a simple connected graph G, Ls(G) is bounded below by the maximal size of a sphere of radius radius(G) around the centres of G.