cliqueFreeOn_of_card_lt

Mathlib.Combinatorics.SimpleGraph.Clique

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

← MathLib Explorer

English

If the cardinality of a finite set s is less than n, then G is n-clique-free on s.

Русский

Если кардинал множества s строго меньше n, то G не содержит n‑клик на s.

LaTeX

$$If $|s| < n$, then $G$ is $n$-clique-free on $s$.$$

Lean4

theorem cliqueFreeOn_of_card_lt {s : Finset α} (h : #s < n) : G.CliqueFreeOn s n := fun _t hts ht =>
  h.not_ge <| ht.2.symm.trans_le <| card_mono hts

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

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

Разделы

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

Аффилиация

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