chromaticNumber_le_of_forall_imp — Mathlib

English

If for every n, G'.Colorable n implies G.Colorable n, then χ(G) ≤ χ(G').

Русский

Если для каждого n верно, что G'.Colorable n ⇒ G.Colorable n, тогда χ(G) ≤ χ(G').

LaTeX

$$$\\big( \\forall n, G'.Colorable n \\rightarrow G.Colorable n \\big) \\Rightarrow G.chromaticNumber \\le G'.chromaticNumber$$$

Lean4

theorem chromaticNumber_le_of_forall_imp {V' : Type*} {G' : SimpleGraph V'} (h : ∀ n, G'.Colorable n → G.Colorable n) :
    G.chromaticNumber ≤ G'.chromaticNumber :=
  by
  rw [chromaticNumber, chromaticNumber]
  simp only [Set.mem_setOf_eq, le_iInf_iff]
  intro m hc
  have := h _ hc
  rw [← chromaticNumber_le_iff_colorable] at this
  exact this

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