free_of_colorable — Mathlib

English

If not H.Colorable n and G.Colorable n, then H.Free G.

Русский

Если H не цветоспособен в n цветах, а G цветоспособен в n цветов, тогда H свободен от включения G.

LaTeX

$$Not (H.Colorable n) \rightarrow G.Colorable n \rightarrow H.Free G$$

Lean4

/-- If `H` is not `n`-colorable and `G` is `n`-colorable, then `G` is `H.Free`. -/
theorem free_of_colorable {W : Type*} {H : SimpleGraph W} (nhc : ¬H.Colorable n) (hc : G.Colorable n) : H.Free G :=
  by
  contrapose! nhc with hc'
  exact ⟨hc.some.comp hc'.some.toHom⟩

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