bot_isCompleteMultipartite

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

English

The bottom element, ⊥, of SimpleGraph is complete multipartite.

Русский

Нижний элемент графового квази-держателя является полным мультитипным графом.

LaTeX

$$$(\bot : SimpleGraph\, \alpha).IsCompleteMultipartite$$$

Lean4

theorem bot_isCompleteMultipartite : (⊥ : SimpleGraph α).IsCompleteMultipartite := by
  simp [IsCompleteMultipartite, Transitive]

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

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

Разделы

Аффилиация

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