of_embedding — Mathlib

English

If there is an embedding f : G.Embedding G' and G'.Colorable n, then G.Colorable n.

Русский

Если существует вложение f: G.Embedding G' и G'.Colorable n, то G.Colorable n.

LaTeX

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

Lean4

@[deprecated SimpleGraph.Colorable.of_hom (since := "2025-09-01")]
theorem of_embedding {V' : Type*} {G' : SimpleGraph V'} (f : G ↪g G') {n : ℕ} (h : G'.Colorable n) : G.Colorable n :=
  Colorable.of_hom f h

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