Formal target: Corpus.PaperKotzigConjecture.kotzig_conjecture

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

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
            (∀ (i : Fin (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 n) 1)) (v : V),
              Eq.{1} (DFunLike.coe.{1, 1, 1} (f i) v) (HAdd.hAdd.{0, 0, 0} (DFunLike.coe.{1, 1, 1} (f 0) v) i))
            (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