Formal target: Corpus.Erdos548.erdos_548

Let $n\geq k+1$.

Exact formal statement

∀ (n k : Nat),
  LE.le.{0} (HAdd.hAdd.{0, 0, 0} k 1) n →
    ∀ (G : SimpleGraph.{0} (Fin n)),
      LE.le.{0}
          (HAdd.hAdd.{0, 0, 0}
            (HMul.hMul.{0, 0, 0} (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (Nat.cast.{0} k) 1) 2) (Nat.cast.{0} n)) 1)
          (Nat.cast.{0} (Set.ncard.{0} (SimpleGraph.edgeSet.{0} G))) →
        ∀ (T : SimpleGraph.{0} (Fin (HAdd.hAdd.{0, 0, 0} k 1))),
          SimpleGraph.IsTree.{0} T → SimpleGraph.IsContained.{0, 0} T G

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record