FormalConjectures/ErdosProblems/268.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos268.erdos_268 sorry line 38 source

   depends on sorry what this means

   Statement uses: Nat, Set.Nonempty, Fin, Real, interior, Set.ofPred, Exists, Set, And, Set.Infinite, Summable, HDiv.hDiv, OfNat.ofNat, Membership.mem, SummationFilter.unconditional, Eq, tsum, HAdd.hAdd

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

   37 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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