erase_of_sup_edge_of_mem — Mathlib

English

If a vertex set s is an n-clique in the graph G with the edge v w added, and v belongs to s, then removing v yields an (n−1)-clique in G.

Русский

Если множество вершин s образует n-клик в графе G с добавленным ребром v w и v ∈ s, то удаление вершины v дает (n−1)-клик в G.

LaTeX

$$$ (G\uplus edge(v,w)).IsNClique(n,s) \land v \in s \Rightarrow G.IsNClique(n-1, s\setminus\{v\}). $$$

Lean4

theorem erase_of_sup_edge_of_mem [DecidableEq α] {v w : α} {s : Finset α} {n : ℕ} (hc : (G ⊔ edge v w).IsNClique n s)
    (hx : v ∈ s) : G.IsNClique (n - 1) (s.erase v)
    where
  isClique := coe_erase v _ ▸ hc.1.sdiff_of_sup_edge
  card_eq := by rw [card_erase_of_mem hx, hc.2]

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