FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 1

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

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture1.conjecture1 sorry line 50 source

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, HSub.hSub, HAdd.hAdd, Fintype.card, OfNat.ofNat, HMul.hMul, Nat, SimpleGraph.matchingNumber, SimpleGraph.Ls

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

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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