mem_cliqueFinset_iff

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

s belongs to G.cliqueFinset n iff s is an n-clique.

Русский

элемент s принадлежит cliqueFinset n тогда, когда s — n-клика.

LaTeX

$$$s \\in G.cliqueFinset n \\iff G.IsNClique n s.$$$

Lean4

@[simp]
theorem mem_cliqueFinset_iff : s ∈ G.cliqueFinset n ↔ G.IsNClique n s :=
  mem_filter.trans <| and_iff_right <| mem_univ _

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

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

Разделы

Аффилиация

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