exists_not_adj_of_cliqueFree_succ

English

If s is an n-clique in G and G is (n+1)-clique-free, then for any x there exists y in s such that x is not adjacent to y.

Русский

Если s образует n‑клик в G и G не содержит клики размера (n+1), то для любого x существует y в s такое, что x не смежен с y.

LaTeX

$$If $G$ is a graph, $s$ is a finite set with $G$-IsNClique of size $n$, and $G$ is clique-free of size $n+1$, then for every $x$ there exists $y\in s$ with $\neg G(x,y)$.$$

Lean4

theorem exists_not_adj_of_cliqueFree_succ (hc : G.IsNClique n s) (h : G.CliqueFree (n + 1)) (x : α) :
    ∃ y, y ∈ s ∧ ¬G.Adj x y := by
  classical
  by_contra! hf
  exact (hc.insert hf).not_cliqueFree h

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