exists_isPathGraph3Compl_of_not_isCompleteMultipartite

English

If G is not complete multipartite, there exist v, w1, w2 with G.IsPathGraph3Compl v w1 w2.

Русский

Если граф G не является complete multipartite, существуют вершины v, w1, w2 такие, что G.IsPathGraph3Compl v w1 w2.

LaTeX

$$∃ v w1 w2, G.IsPathGraph3Compl v w1 w2$$

Lean4

theorem exists_isPathGraph3Compl_of_not_isCompleteMultipartite (h : ¬IsCompleteMultipartite G) :
    ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂ :=
  by
  rw [IsCompleteMultipartite, Transitive] at h
  push_neg at h
  obtain ⟨_, _, _, h1, h2, h3⟩ := h
  rw [adj_comm] at h1
  exact ⟨_, _, _, h3, h1, h2⟩

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