theorem WrittenOnTheWallII.GraphConjecture2.conjecture2 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) : 2 * (G.l - 1) ≤ G.Ls

WOWII Conjecture 2

For a simple connected graph G, Ls(G) ≥ 2 · (l(G) - 1) where l(G) is the average independence number of the neighbourhoods of the vertices of G.