isBipartiteWith_support_subset — Mathlib

English

If G is bipartite with s,t, then the support of G is contained in s ∪ t.

Русский

Если G двудольный с s и t, тогда опора графа лежит в s ∪ t.

LaTeX

$$G.IsBipartiteWith s t → G.support ⊆ s ∪ t$$

Lean4

/-- If `G.IsBipartiteWith s t`, then the support of `G` is a subset of `s ∪ t`. -/
theorem isBipartiteWith_support_subset (h : G.IsBipartiteWith s t) : G.support ⊆ s ∪ t :=
  by
  intro v ⟨w, hadj⟩
  apply h.mem_of_adj at hadj
  tauto

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