FormalConjectures/ErdosProblems/73.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 73

References:

Imports (1)
  1. theorem Erdos73.erdos_73 sorry line 46 source

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Exists, Fintype, SimpleGraph, Finset, And, LE.le, Eq, Set, Sym2, SimpleGraph.edgeSet, SimpleGraph.induce, EmptyCollection.emptyCollection, GE.ge, Real, Finset.card, HDiv.hDiv, HSub.hSub and 3 more

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

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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