colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree

English

Definition: G.FiveWheelLikeFree r k means there is no IsFiveWheelLike r k structure in G.

Русский

Определение: G.FiveWheelLikeFree r k означает, что в G нет структуры IsFiveWheelLike r k.

LaTeX

$$$$ \\text{FiveWheelLikeFree}(G,r,k) := \\forall {v,w_1,w_2,s,t}, \\neg G.IsFiveWheelLike r k v w_1 w_2 s t. $$$$

Lean4

/-- A maximally `Kᵣ₊₁`-free graph is `r`-colorable iff it is complete-multipartite. -/
theorem colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree (h : Maximal (fun H => H.CliqueFree (r + 1)) G) :
    G.Colorable r ↔ G.IsCompleteMultipartite := by
  match r with
  | 0 => exact ⟨fun _ ↦ fun x ↦ cliqueFree_one.1 h.1 |>.elim' x, fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩
  | r + 1 =>
    refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩
    contrapose! hc
    obtain ⟨_, _, _, _, _, hw⟩ := exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
    exact hw.not_colorable_succ

Похожие утверждения