colorable_zero_iff

Mathlib.Combinatorics.SimpleGraph.Coloring

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

English

G.Colorable 0 if and only if IsEmpty V.

Русский

G.Colorable 0 тогда и только тогда IsEmpty V.

LaTeX

$$$G.Colorable 0 \\iff IsEmpty V$$$

Lean4

@[simp]
theorem colorable_zero_iff : G.Colorable 0 ↔ IsEmpty V :=
  ⟨G.isEmpty_of_colorable_zero, fun _ ↦ G.colorable_of_isEmpty 0⟩

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

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

Разделы

Аффилиация

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