Formal target: Corpus.Erdos1020.erdos_1020

Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges.

Exact formal statement

∀ (r : Nat),
  LE.le.{0} 3 r →
    ∀ (n k : Nat),
      LT.lt.{0} 0 k →
        LE.le.{0} (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} r k) 1) n →
          Eq.{1} (Corpus.Erdos1020.f n r k)
            (Max.max.{0} ((HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} r k) 1).choose r)
              (HSub.hSub.{0, 0, 0} (n.choose r) ((HAdd.hAdd.{0, 0, 0} (HSub.hSub.{0, 0, 0} n k) 1).choose r)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record