FormalConjectures/WrittenOnTheWallII/GraphConjecture316.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 316

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

Imports (1)
Imported by 1 file
  1. theorem WrittenOnTheWallII.GraphConjecture316.conjecture316 sorry line 48 source

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Rat, SimpleGraph.averageDegree, Compl.compl, Finset.card, SimpleGraph.pendantVertices, SimpleGraph.IsWellTotallyDominated

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

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. example WrittenOnTheWallII.GraphConjecture316.(example at line 57) line 57 source

    Source documentation

    The average degree of the edgeless graph on 3 vertices is 0.

    example : averageDegree (⊥ : SimpleGraph (Fin 3)) = 0 := by
…
  3. example WrittenOnTheWallII.GraphConjecture316.(example at line 62) line 62 source

    Source documentation

    In P₃ (path 0-1-2), the average degree is 4/3 and there are 2 pendant vertices.

    example : averageDegree (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 4/3 := by
…