isBipartiteWith_neighborSet' — Mathlib

English

If G is bipartite with s,t and w ∈ t, then neighborSet(w) = {v ∈ s | G.Adj v w}.

Русский

Если G двудольный с s и t и w ∈ t, то neighborSet(w) = {v ∈ s | Adj(v,w)}.

LaTeX

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

Lean4

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

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