FormalConjectures/WrittenOnTheWallII/GraphConjecture142.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 142

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

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture142.conjecture142 sorry line 82 source

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Set, SimpleGraph.maxEccentricityVertices, LE.le, Real, HAdd.hAdd, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Nat, SimpleGraph.girth, SimpleGraph.eccSet, SimpleGraph.largestInducedTreeSize

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

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. example WrittenOnTheWallII.GraphConjecture142.(example at line 91) line 91 source

    Source documentation

    The largestInducedTreeSize is nonneg.

    example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
…
  3. example WrittenOnTheWallII.GraphConjecture142.(example at line 95) line 95 source

    Source documentation

    eccSet G returns a natural number (nonneg).

    example (G : SimpleGraph (Fin 3)) [DecidableRel G.Adj] :
    0 ≤ eccSet G (maxEccentricityVertices G) :=
…