cliqueFreeOn_singleton

Mathlib.Combinatorics.SimpleGraph.Clique

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

← MathLib Explorer

English

G.CliqueFreeOn {a} n is equivalent to 1 < n.

Русский

G.CliqueFreeOn {a} n эквивалентно 1 < n.

LaTeX

$$For any graph $G$ and vertex $a$, $G$ is $n$-clique-free on the singleton \{a\} iff $1 < n$.$$

Lean4

@[simp]
theorem cliqueFreeOn_singleton : G.CliqueFreeOn { a } n ↔ 1 < n := by
  obtain _ | _ | n := n <;> simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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