of_hom

Mathlib.Combinatorics.SimpleGraph.Coloring

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Colorable.of_hom

English

If there exists a homomorphism f : G →g G' and G'.Colorable n, then G.Colorable n.

Русский

Если существует гомоморфизм f: G →g G' и G'.Colorable n, то G.Colorable n.

LaTeX

$$$(\\exists f : G \\to_g G')\\ G'.Colorable n \\Rightarrow G.Colorable n$$$

Lean4

theorem of_hom {V' : Type*} {G' : SimpleGraph V'} (f : G →g G') {n : ℕ} (h : G'.Colorable n) : G.Colorable n :=
  ⟨(h.toColoring (by simp)).comp f⟩

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

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

Разделы

Аффилиация

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