not_isCompleteMultipartite_of_pathGraph3ComplEmbedding

English

For every embedding e of the complement of the path on three vertices into G, G is not a complete multipartite graph.

Русский

Для каждого вложения e комплемента графа пути из трёх вершин в G граф G не является полным мультитипным графом.

LaTeX

$$∀ e:(pathGraph\,3)^{\mathrm{c}} \hookrightarrow G, ¬IsCompleteMultipartite(G)$$

Lean4

theorem not_isCompleteMultipartite_of_pathGraph3ComplEmbedding (e : (pathGraph 3)ᶜ ↪g G) : ¬IsCompleteMultipartite G :=
  by
  intro h
  have h0 : ¬G.Adj (e 0) (e 1) := by simp [pathGraph_adj]
  have h1 : ¬G.Adj (e 1) (e 2) := by simp [pathGraph_adj]
  have h2 : G.Adj (e 0) (e 2) := by simp [pathGraph_adj]
  exact h h0 h1 h2

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