English
Let G be maximal with respect to the property of being (n+1)-clique-free. If x ≠ y and x,y are not adjacent in G, then there exists a subset s disjoint from {x,y} such that both x ∪ s and y ∪ s form n-cliques in G.
Русский
Пусть G максимально по отношению к свойству отсутствия (n+1)-клик. Если x ≠ y и x не смежно с y, то существует множество s, не содержащее x и y, такое что x ∪ s и y ∪ s образуют клики размером n в G.
LaTeX
$$Let $G$ be a graph with maximal property that all its subgraphs are not containing an $(n+1)$-clique. If $x\neq y$ and $\lnot G(x,y)$, then there exists a set $s$ with $x,y\notin s$ such that $G$ has $n$-cliques on $insert x s$ and on $insert y s$.$$
Lean4
theorem exists_of_maximal_cliqueFree_not_adj [DecidableEq α] (h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G) {x y : α}
(hne : x ≠ y) (hn : ¬G.Adj x y) : ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s) :=
by
obtain ⟨t, hc⟩ := not_forall_not.1 <| h.not_prop_of_gt <| G.lt_sup_edge _ _ hne hn
use (t.erase x).erase y, erase_right_comm (a := x) ▸ (notMem_erase _ _), notMem_erase _ _
have h1 := h.1.mem_of_sup_edge_isNClique hc
have h2 := h.1.mem_of_sup_edge_isNClique (edge_comm .. ▸ hc)
rw [insert_erase <| mem_erase_of_ne_of_mem hne.symm h2, erase_right_comm,
insert_erase <| mem_erase_of_ne_of_mem hne h1]
exact ⟨(edge_comm .. ▸ hc).erase_of_sup_edge_of_mem h2, hc.erase_of_sup_edge_of_mem h1⟩
