map — Mathlib

English

If G is n-colorable, then mapping the vertices along an embedding f yields a graph (G.map f) that is also n-colorable.

Русский

Если G цветоразрешим при n цветах, то отображение вершин через вложение f сохраняет цветность: (G.map f).Colorable n.

LaTeX

$$$G.Colorable n \\rightarrow (G.map\\ f).Colorable n$$$

Lean4

/-- If `G` is `n`-colorable, then mapping the vertices of `G` produces an `n`-colorable simple
graph. -/
theorem map {β : Type*} (f : V ↪ β) [NeZero n] {G : SimpleGraph V} (hc : G.Colorable n) : (G.map f).Colorable n :=
  by
  obtain ⟨C⟩ := hc
  use extend f C (const β default)
  intro a b ⟨_, _, hadj, ha, hb⟩
  rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
  exact C.valid hadj

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