colorable_iff_forall_connectedComponents

English

A graph G is n-colorable if and only if every connected component of G, when considered as a separate simple graph, is n-colorable.

Русский

Граф G можно окрасить в n цветов тогда и только тогда каждая компонентa связности G может быть окрашена в n цветов.

LaTeX

$$$G.Colorable\\ n \\iff \\forall c : G.ConnectedComponent, (c.toSimpleGraph).Colorable n$$$

Lean4

theorem colorable_iff_forall_connectedComponents {n : ℕ} :
    G.Colorable n ↔ ∀ c : G.ConnectedComponent, (c.toSimpleGraph).Colorable n :=
  ⟨fun ⟨C⟩ _ ↦ ⟨fun v ↦ C v, fun h h1 ↦ C.valid h h1⟩, fun h ↦ ⟨G.homOfConnectedComponents (fun c ↦ (h c).some)⟩⟩

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