theorem WrittenOnTheWallII.GraphConjecture19.conjecture19 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [Nontrivial α] (h_conn : G.Connected) : SimpleGraph.FLOOR (↑(∑ v : Set α, G.ecc v) / ↑(Fintype.card α) + sSup (Set.range G.indepNeighbors)) ≤ G.b

WOWII Conjecture 19

If G is connected then the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ FLOOR((∑ ecc(v))/(|V|) + sSup (range (l G))), where ecc(v) denotes eccentricity and l(G) is the independence number of neighbourhoods.