turanGraph_zero

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

English

For any n, turanGraph(n,0) equals the top graph (complete graph).

Русский

Для любого n граф Турэна с параметром 0 равен полному графу.

LaTeX

$$$\mathrm{turanGraph}(n,0) = \top.$$$

Lean4

@[simp]
theorem turanGraph_zero : turanGraph n 0 = ⊤ := by ext a b;
  simp_rw [turanGraph, top_adj, Nat.mod_zero, not_iff_not, Fin.val_inj]

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

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

Разделы

Аффилиация

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