Formal target: Corpus.PaperRingelConjecture.ringel_conjecture

For any tree $T$ with $n$ edges, the complete graph $K_{2n+1}$ decomposes into $2n+1$ edge-disjoint copies of $T$.

Exact formal statement

∀ {V : Type} [Finite.{1} V] (T : SimpleGraph.{0} V),
  SimpleGraph.IsTree.{0} T →
    ∀ (n : Nat),
      Eq.{1} (Set.ncard.{0} (SimpleGraph.edgeSet.{0} T)) n →
        Exists.{1} fun f =>
          And
            (Pairwise.{0} fun i j =>
              Disjoint.{0} (SimpleGraph.edgeSet.{0} (SimpleGraph.map.{0, 0} (DFunLike.coe.{1, 1, 1} (f i)) T))
                (SimpleGraph.edgeSet.{0} (SimpleGraph.map.{0, 0} (DFunLike.coe.{1, 1, 1} (f j)) T)))
            (Eq.{1} (iSup.{0, 1} fun i => SimpleGraph.map.{0, 0} (DFunLike.coe.{1, 1, 1} (f i)) T) Top.top.{0})

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record