FormalConjectures/WrittenOnTheWallII/GraphConjecture438b.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 438b

Reference:E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

WOWII 438b asks whether

alpha₂(G) ≤ alpha(G) + alpha(G[V \ H₂]) + |E(G[H₂])|,

where H₂ is the set of vertices of degree at most two. The conjecture is true. In fact, the same inequality holds with an arbitrary vertex subset in place of H₂.

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture438b.conjecture438b sorry line 49 source

    depends on sorry what this means

    Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LT.lt, Nat, OfNat.ofNat, Fintype.card, LE.le, SimpleGraph.alphaTwo, HAdd.hAdd, SimpleGraph.indepNum, SimpleGraph.indepNumOn, SDiff.sdiff, Finset, Finset.univ and 4 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.