isClique_sup_edge_of_ne_iff — Mathlib

English

For v ≠ w, (G ⊔ edge v w).IsClique s holds exactly when G.IsClique(s \\ {v}) and G.IsClique(s \\ {w}).

Русский

Для v ≠ w, (G ⊔ edge v w).IsClique s эквивалентно тому, что G.IsClique(s \\ {v}) и G.IsClique(s \\ {w}).

LaTeX

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

Lean4

theorem isClique_sup_edge_of_ne_iff {v w : α} {s : Set α} (h : v ≠ w) :
    (G ⊔ edge v w).IsClique s ↔ G.IsClique (s \ { v }) ∧ G.IsClique (s \ { w }) :=
  ⟨fun h' ↦ ⟨h'.sdiff_of_sup_edge, (edge_comm .. ▸ h').sdiff_of_sup_edge⟩, fun h' ↦
    isClique_sup_edge_of_ne_sdiff h h'.1 h'.2⟩

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