Formal target: Corpus.Erdos143.erdos_143.parts.ii

Or $$ \sum_{x \in A} \frac{1}{x \log x} < \infty, $$

Exact formal statement

∀ (A : Set.{0} Real),
  Corpus.Erdos143.WellSeparatedSet A →
    Summable.{0, 0} fun x =>
      HDiv.hDiv.{0, 0, 0} 1 (HMul.hMul.{0, 0, 0} (Subtype.val.{1} x) (Real.log (Subtype.val.{1} x)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record