Formal target: Corpus.Erdos324.erdos_324.variants.quintic

Probably $f(x) = x^5$ has the property that the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct.

Exact formal statement

Set.InjOn.{0, 0}
  (fun x =>
    Corpus.Erdos324.erdos_324.variants.quintic.match_1.{1} (fun x => Nat) x fun a b =>
      HAdd.hAdd.{0, 0, 0} (HPow.hPow.{0, 0, 0} a 5) (HPow.hPow.{0, 0, 0} b 5))
  (Set.ofPred.{0} fun x =>
    Corpus.Erdos324.erdos_324.variants.quintic.match_1.{1} (fun x => Prop) x fun a b => LT.lt.{0} a b)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record