isMaximalClique_iff — Mathlib

English

A clique s is maximal iff it is a clique and no strictly larger clique contains it.

Русский

Клика s максимальна тогда, когда она является кликой и не существует клики t, содержащей s, с $s \subset t$.

LaTeX

$$$\\text{Maximal } G.IsClique\\ s \\iff G.IsClique\\ s \\wedge \\forall t \\subseteq V,\\ G.IsClique\\ t \\to s \\subseteq t \\to t \\subseteq s.$$$

Lean4

/-- A maximal clique in a graph `G` is a clique that cannot be extended by adding more vertices. -/
theorem isMaximalClique_iff {s : Set α} :
    Maximal G.IsClique s ↔ G.IsClique s ∧ ∀ t : Set α, G.IsClique t → s ⊆ t → t ⊆ s :=
  Iff.rfl

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