instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj

Mathlib.Combinatorics.SimpleGraph.Clique

URI: https://scilib.ai/kg/mathlib#SimpleGraph.instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj

English

A set s is NClique for n if and only if s is empty and n = 0 when s is empty.

Русский

Для множества s: s пусто тогда и только тогда, когда n = 0.

LaTeX

$$$$(⊥).IsNClique n s \\iff n ≤ 1 \\land \\#s = n$$$$

Lean4

instance [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} : Decidable (G.IsNClique n s) :=
  decidable_of_iff' _ G.isNClique_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru