sup_edge — Mathlib

English

If a graph G has no n-cliques, then the graph obtained by adding a single edge between two vertices has no (n+1)-cliques.

Русский

Если граф G не содержит n-клик, то граф, полученный добавлением одного ребра между двумя вершинами, не содержит (n+1)-клик.

LaTeX

$$$G$ is a simple graph; if $G$ is $n$-clique-free, then $(G \cup \{\{v,w\}\})$ is $(n+1)$-clique-free.$$

Lean4

/-- Adding an edge increases the clique number by at most one. -/
protected theorem sup_edge (h : G.CliqueFree n) (v w : α) : (G ⊔ edge v w).CliqueFree (n + 1) := fun _ hs ↦
  (hs.erase_of_sup_edge_of_mem <| (h.mono n.le_succ).mem_of_sup_edge_isNClique hs).not_cliqueFree h

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