sdiff_of_sup_edge — Mathlib

English

If v ≠ w and the restrictions of a set s removing each of v or w are cliques in G, then the union with edge v w forms a clique in the supremum of G and the edge v w.

Русский

Если вершины v и w различны, и s без {v} и s без {w} являются кликами в G, то объединение с ребром v w образует clique в графе, добавляющем ребро v w.

LaTeX

$$$$ \\forall x,y, x,y \\in s \\Rightarrow \\text{adj}_{G\\⊔\\text{edge }v w}(x,y) $$$$

Lean4

theorem sdiff_of_sup_edge {v w : α} {s : Set α} (hc : (G ⊔ edge v w).IsClique s) : G.IsClique (s \ { v }) :=
  by
  intro _ hx _ hy hxy
  have := hc hx.1 hy.1 hxy
  simp_all [sup_adj, edge_adj]

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