maximumClique_exists

Mathlib.Combinatorics.SimpleGraph.Clique

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

← MathLib Explorer

English

There exists a maximum clique in G.

Русский

Существует максимальная клика в графе G.

LaTeX

$$$\\exists s : Finset \\alpha,\\ G.IsMaximumClique s.$$$

Lean4

theorem maximumClique_exists [Fintype α] : ∃ (s : Finset α), G.IsMaximumClique s :=
  by
  obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum
  exact ⟨s, ⟨snc.isClique, fun t ht => snc.card_eq.symm ▸ ht.card_le_cliqueNum⟩⟩

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

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

Разделы

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

Аффилиация

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