isNClique_bot_iff — Mathlib

English

G.IsNClique 3 s holds exactly when there exist vertices a,b,c with mutual adjacencies and s equals {a,b,c}.

Русский

G.IsNClique 3 s выполняется тогда и только тогда, когда существуют вершины a,b,c взаимно смежные, и множество s равно {a,b,c}.

LaTeX

$$$$ G.IsNClique 3 s \\iff \\exists a,b,c,\\ G.Adj a b \\land G.Adj a c \\land G.Adj b c \\land s = \\{a,b,c\\} $$$$

Lean4

@[simp]
theorem isNClique_bot_iff : (⊥ : SimpleGraph α).IsNClique n s ↔ n ≤ 1 ∧ #s = n :=
  by
  rw [isNClique_iff, isClique_bot_iff]
  refine and_congr_left ?_
  rintro rfl
  exact card_le_one.symm

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