not_isClique_iff — Mathlib

English

¬ G.IsClique s holds exactly when there exist v,w ∈ s with v ≠ w and ¬ G.Adj v w.

Русский

Не является кликой графа гov s тогда и только тогда, когда существуют v,w ∈ s такие, что v ≠ w и ¬ G.Adj v w.

LaTeX

$$$ \neg G.IsClique s \iff \exists v,w \in s, v \neq w \land \neg G.Adj v w $$$

Lean4

theorem not_isClique_iff : ¬G.IsClique s ↔ ∃ (v w : s), v ≠ w ∧ ¬G.Adj v w := by
  aesop (add simp [isClique_iff, Set.Pairwise])

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