mem_of_sup_edge_isNClique — Mathlib

English

Let G be an n-clique-free graph. If the graph obtained by adding the edge {x,y} to G contains an n-vertex clique on t, then x ∈ t.

Русский

Пусть G — граф без n-клики. Если граф, полученный добавлением ребра {x,y} к G, содержит n‑вершину клику на множестве вершин t, то x ∈ t.

LaTeX

$$$G$ is a simple graph on some set $\alpha$; if $G$ is $n$-clique-free and $(G \cup \{\{x,y\}\})$ has an $n$-clique on $t$, then $x \in t$.$$

Lean4

theorem mem_of_sup_edge_isNClique {x y : α} {t : Finset α} {n : ℕ} (h : G.CliqueFree n)
    (hc : (G ⊔ edge x y).IsNClique n t) : x ∈ t := by
  by_contra! hf
  have ht : (t : Set α) \ { x } = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
  exact h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩

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