FormalConjectures/ErdosProblems/341.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 341

References:

Imports (1)
  1. theorem Erdos341.erdos_341 sorry line 54 source

    depends on sorry what this means

    Statement uses: Iff, False, Nat, Int, Filter.Eventually, IsLeast, Set.ofPred, And, LT.lt, Not, Membership.mem, Set, Exists, LE.le, Eq, HAdd.hAdd, OfNat.ofNat, Filter.atTop, HSub.hSub, GT.gt

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

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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