FormalConjectures/WrittenOnTheWallII/GraphConjecture59.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 59

References:

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture59.conjecture59 sorry line 59 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, Int.ceil, Real.sqrt, HMul.hMul, SimpleGraph.residue, SimpleGraph.b, SimpleGraph.largestInducedForestSize

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

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. example WrittenOnTheWallII.GraphConjecture59.(example at line 69) line 69 source

    Source documentation

    The largestInducedForestSize is nonneg.

    example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedForestSize := Nat.zero_le _
…
  3. example WrittenOnTheWallII.GraphConjecture59.(example at line 74) line 74 source

    Source documentation

    The residue of $K_2$ equals $1$: degree sequence is $[1, 1]$; one Havel-Hakimi step gives $[0]$, leaving a single zero.

    example : residue (⊤ : SimpleGraph (Fin 2)) = 1 := by
…