isBipartite_iff_exists_isBipartiteWith

English

If G.IsBipartiteWith s t, then the sum of the degrees of vertices in t equals the number of edges.

Русский

Если G двудольный с частями s и t, тогда сумма степеней вершин в t равна числу ребер.

LaTeX

$$$\sum_{v \in t} G.degree(v) = \#G.edgeFinset$$$

Lean4

/-- `G.IsBipartite` if and only if `G.IsBipartiteWith s t`. -/
theorem isBipartite_iff_exists_isBipartiteWith : G.IsBipartite ↔ ∃ s t : Set V, G.IsBipartiteWith s t :=
  ⟨IsBipartite.exists_isBipartiteWith, fun ⟨_, _, h⟩ ↦ h.isBipartite⟩

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