theorem WrittenOnTheWallII.GraphConjecture40.conjecture40 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h_conn : G.Connected) (h_nontrivial : 1 < Fintype.card α) : ↑⌈(G.p + G.b + 1) / 2⌉ ≤ G.f

WOWII Conjecture 40

For a nontrivial connected graph G the size f(G) of a largest induced forest satisfies f(G) ≥ ceil((p(G) + b(G) + 1)/2) where p(G) is the path cover number and b(G) is the largest induced bipartite subgraph size.