isMaximumClique_iff — Mathlib

English

A clique s is maximum iff s is a clique and any clique t is no larger than s.

Русский

Клика s является максимальной тогда и только тогда, когда она клика и любая клика t имеет не больший размер, чем s.

LaTeX

$$$G.IsMaximumClique\\ s \\iff \\bigl( G.IsClique\\ s \\wedge \\forall t : Finset \\alpha,\\ G.IsClique\\ t \\to \\#t \\le \\#s \\bigr).$$$

Lean4

theorem isMaximumClique_iff [Fintype α] {s : Finset α} :
    G.IsMaximumClique s ↔ G.IsClique s ∧ ∀ t : Finset α, G.IsClique t → #t ≤ #s :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

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