English
Any maximally K_r+2-free graph not complete multipartite contains a maximal IsFiveWheelLike structure W_r,k for some k < r.
Русский
Любой максимальный по отношению к K_r+2-безграфности граф, не являющийся полным multipartite, содержит максимальную структуру IsFiveWheelLike W_r,k для некоторого k<r.
LaTeX
$$$$ \\exists k,v,w_1,w_2,s,t:\\; G.IsFiveWheelLike r k v w_1 w_2 s t \\wedge k < r \\wedge \\forall j, k < j \\Rightarrow G.FiveWheelLikeFree r j. $$$$
Lean4
/-- Any maximally `Kᵣ₊₂`-free graph that is not complete-multipartite contains a maximal
`IsFiveWheelLike` structure `Wᵣ,ₖ` for some `k < r`. (It is maximal in terms of `k`.)
-/
theorem exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite
(h : Maximal (fun H => H.CliqueFree (r + 2)) G) (hnc : ¬G.IsCompleteMultipartite) :
∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ j, k < j → G.FiveWheelLikeFree r j :=
by
obtain ⟨_, _, _, s, t, hw⟩ := exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hnc
let P : ℕ → Prop := fun k ↦ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t
have hk : P #(s ∩ t) := ⟨_, _, _, _, _, hw⟩
classical
obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk
exact
⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1, fun _ hj _ _ _ _ _ hv ↦
hj.not_ge <| Nat.le_findGreatest (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩
