isClique_insert_of_notMem — Mathlib

English

If a is not in s, then G.IsClique (insert a s) iff G.IsClique s and ∀ b ∈ s, G.Adj a b.

Русский

Если a не принадлежит s, то G.IsClique (insert a s) эквивалентно G.IsClique s и ∀ b ∈ s, G.Adj a b.

LaTeX

$$$ a \notin s \rightarrow (G.IsClique (insert a s) \iff G.IsClique s \land \forall b \in s, G.Adj a b) $$$

Lean4

theorem isClique_insert_of_notMem (ha : a ∉ s) : G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b :=
  Set.pairwise_insert_of_symmetric_of_notMem G.symm ha

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