English
If G is maximal with respect to being K_r+2-free and not complete multipartite, there exist vertices v, w1, w2 and subgraphs s, t such that G contains a FiveWheelLike structure with parameters r and some k < r, together with a universality property for larger k.
Русский
Если граф G максимален по свойству K_r+2-безграфности и не является полным multipartite, существуют вершины v, w1, w2 и подгруппы s, t так, что G содержит структуру FiveWheelLike с параметрами r и некоторым k < r, а также характеристику, распространяющуюся на большие k.
LaTeX
$$$$ \\exists k\\, \\exists v,w_1,w_2,s,t\\, (G.IsFiveWheelLike\\; r\\; k\\; v\\; w_1\\; w_2\\; s\\; t) \\land k < r \\land \\forall j, k < j \\Rightarrow G.FiveWheelLikeFree\\; r\\; j. $$$$
Lean4
theorem exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite
(h : Maximal (fun H => H.CliqueFree (r + 2)) G) (hnc : ¬G.IsCompleteMultipartite) :
∃ v w₁ w₂ s t, G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t :=
by
obtain ⟨v, w₁, w₂, p3⟩ := exists_isPathGraph3Compl_of_not_isCompleteMultipartite hnc
obtain ⟨s, h1, h2, h3, h4⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_fst p3.not_adj_fst
obtain ⟨t, h5, h6, h7, h8⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_snd p3.not_adj_snd
exact ⟨_, _, _, _, _, p3, h1, h5, h2, h6, h3, h4, h7, h8, rfl⟩
