isBipartiteWith_neighborSet — Mathlib

English

If G is bipartite with s,t and v ∈ s, then the neighbor set of v equals { w ∈ t | G.Adj v w }.

Русский

Если G двудольный с s и t и v ∈ s, то множество соседей v равно { w ∈ t | G.Adj v w }.

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.neighborSet(v) = { w ∈ t | G.Adj v w }$$

Lean4

/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is the set of vertices in
`t` adjacent to `v` in `G`. -/
theorem isBipartiteWith_neighborSet (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G.neighborSet v = {w ∈ t | G.Adj v w} :=
  by
  ext w
  rw [mem_neighborSet, Set.mem_setOf_eq, iff_and_self]
  exact h.mem_of_mem_adj hv

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