Formal target: Corpus.Erdos41.erdos_41

Let $A \subset \mathbb{N}$ be an infinite set such that the triple sums $a+b+c$ are all distinct for $a,b,c \in A$ (aside from the trivial coincidences).

Exact formal statement

∀ (A : Set.{0} Nat),
  Corpus.Erdos41.NtupleCondition A 3 →
    Set.Infinite.{0} A →
      Eq.{1}
        (Filter.liminf.{0, 0}
          (fun N =>
            HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Set.ncard.{0} (Inter.inter.{0} A (Set.Icc.{0} 1 N))))
              (HPow.hPow.{0, 0, 0} (Nat.cast.{0} N) (1 / 3)))
          Filter.atTop.{0})
        0

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record