exists_isBipartiteWith — Mathlib

English

If a simple graph G is bipartite, then there exist disjoint sets s and t such that every edge of G connects a vertex in s with a vertex in t.

Русский

Если граф G двудольный, то существуют непересекающиеся множества S и T такие, что каждое ребро соединяет вершину из S с вершиной из T.

LaTeX

$$∃ S T, G.IsBipartiteWith S T$$

Lean4

/-- If a simple graph `G` is bipartite, then there exist disjoint sets `s` and `t`
such that all edges in `G` connect a vertex in `s` to a vertex in `t`. -/
theorem exists_isBipartiteWith (h : G.IsBipartite) : ∃ s t, G.IsBipartiteWith s t :=
  by
  obtain ⟨c, hc⟩ := h
  refine ⟨{v | c v = 0}, {v | c v = 1}, by aesop (add simp [Set.disjoint_left]), ?_⟩
  rintro v w hvw
  apply hc at hvw
  simp [Set.mem_setOf_eq] at hvw ⊢
  cutsat

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