Formal target: Corpus.Erdos628.erdos_628

Let $G$ be a graph with chromatic number $k$ containing no $K_k$.

Exact formal statement

∀ (V : Type u_1) [Fintype.{u_1} V] (G : SimpleGraph.{u_1} V) (k : Nat),
  Eq.{1} (SimpleGraph.chromaticNumber.{u_1} G) (Nat.cast.{0} k) →
    SimpleGraph.CliqueFree.{u_1} G k →
      ∀ (a b : Nat),
        GE.ge.{0} a 2 →
          GE.ge.{0} b 2 →
            Eq.{1} (HAdd.hAdd.{0, 0, 0} a b) (HAdd.hAdd.{0, 0, 0} k 1) →
              Exists.{u_1 + 1} fun s =>
                And (GE.ge.{0} (SimpleGraph.chromaticNumber.{u_1} (SimpleGraph.induce.{u_1} s G)) (Nat.cast.{0} a))
                  (GE.ge.{0} (SimpleGraph.chromaticNumber.{u_1} (SimpleGraph.induce.{u_1} (Compl.compl.{u_1} s) G))
                    (Nat.cast.{0} b))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record