isCompleteMultipartite_iff — Mathlib

English

A graph is complete multipartite if and only if it is isomorphic to some completeMultipartiteGraph V.

Русский

Граф является полным мультитипным тогда и только тогда, когда он изоморфен некоторому графу completeMultipartiteGraph V.

LaTeX

$$$G.IsCompleteMultipartite \iff \exists ι\; (V : ι \to Type)\; (Nonempty (V i))\; \text{and } Nonempty (G \cong_g completeMultipartiteGraph V)$$$

Lean4

theorem isCompleteMultipartite_iff :
    G.IsCompleteMultipartite ↔
      ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ i, Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V) :=
  by
  constructor <;> intro h
  · exact ⟨_, _, fun _ ↦ ⟨_, h.setoid.refl _⟩, ⟨h.iso⟩⟩
  · obtain ⟨_, _, _, ⟨e⟩⟩ := h
    intro _ _ _ h1 h2
    rw [← e.map_rel_iff] at *
    exact completeMultipartiteGraph.isCompleteMultipartite _ h1 h2

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