FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 327

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

Imports (1)
Imported by 1 file
  1. theorem WrittenOnTheWallII.GraphConjecture327.conjecture327 sorry line 69 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Eq, Nat, HMul.hMul, OfNat.ofNat, SimpleGraph.dominationNumber, SimpleGraph.indepDominationNumber, SimpleGraph.IsWellTotallyDominated

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

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. example WrittenOnTheWallII.GraphConjecture327.(example at line 79) line 79 source

    Source documentation

    In K₂, the max degree is 1 (each vertex has exactly one neighbor).

    example : (⊤ : SimpleGraph (Fin 2)).maxDegree = 1 := by decide
…
  3. example WrittenOnTheWallII.GraphConjecture327.(example at line 83) line 83 source

    Source documentation

    In the path graph P₃, vertex 1 has degree 2.

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