English
Let G be a simple graph. If G is not complete multipartite, then G contains a subgraph isomorphic to the complement of the path on three vertices; equivalently, there exists an embedding of the complement of pathGraph(3) into G.
Русский
Пусть G — простейший граф. Если G не является полно-мультитипным графом, то в G содержится подправая, изоморфная комплементу графа пути с тремя вершинами; эквивалентно существует вложение комплемента pathGraph(3) в G.
LaTeX
$$$\neg\,G.IsCompleteMultipartite \Rightarrow \exists e:\,(pathGraph\,3)^{\mathrm{c}} \hookrightarrow G$$$
Lean4
/-- Embedding of `(pathGraph 3)ᶜ` into `G` that is not complete-multipartite. -/
noncomputable def pathGraph3ComplEmbeddingOf (h : ¬G.IsCompleteMultipartite) : (pathGraph 3)ᶜ ↪g G :=
IsPathGraph3Compl.pathGraph3ComplEmbedding
(exists_isPathGraph3Compl_of_not_isCompleteMultipartite h).choose_spec.choose_spec.choose_spec
