not_isCompleteMultipartite_iff_exists_isPathGraph3Compl

English

¬IsCompleteMultipartite G iff ∃ v w1 w2, G.IsPathGraph3Compl v w1 w2.

Русский

¬IsCompleteMultipartite G тогда и только тогда, когда существует v, w1, w2 такие, что G.IsPathGraph3Compl v w1 w2.

LaTeX

$$¬G.IsCompleteMultipartite G ↔ ∃ v w1 w2, G.IsPathGraph3Compl v w1 w2$$

Lean4

theorem not_isCompleteMultipartite_iff_exists_isPathGraph3Compl :
    ¬IsCompleteMultipartite G ↔ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂ :=
  ⟨fun h ↦ G.exists_isPathGraph3Compl_of_not_isCompleteMultipartite h, fun ⟨_, _, _, h1, h2, h3⟩ ↦ fun h ↦
    h (by rwa [adj_comm] at h2) h3 h1⟩

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