isClique_sup_edge_of_ne_sdiff — Mathlib

English

For distinct v, w, the clique condition for G ⊔ edge v w on s is equivalent to both s \ {v} and s \ {w} being cliques in G.

Русский

Для различных v, w условие клики для G ⊔ edge v w на s эквивалентно тому, что s без v и без w являются кликами в G.

LaTeX

$$$$ (G \\ ⊔\\ edge\\ v\\ w).IsClique\\ s \\iff G.IsClique(s \\ {v}) \\land G.IsClique(s \\ {w}) $$$$

Lean4

theorem isClique_sup_edge_of_ne_sdiff {v w : α} {s : Set α} (h : v ≠ w) (hv : G.IsClique (s \ { v }))
    (hw : G.IsClique (s \ { w })) : (G ⊔ edge v w).IsClique s :=
  by
  intro x hx y hy hxy
  by_cases h' : x ∈ s \ { v } ∧ y ∈ s \ { v } ∨ x ∈ s \ { w } ∧ y ∈ s \ { w }
  · obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
    · exact hv.mono le_sup_left hx hy hxy
    · exact hw.mono le_sup_left hx hy hxy
  · exact Or.inr ⟨by by_cases x = v <;> aesop, hxy⟩

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