isBipartiteWith_neighborFinset — Mathlib

English

Same as above, framed as a version of the prime variant.

Русский

Та же формулировка в виде второй версии.

LaTeX

$$G.IsBipartiteWith s t → w ∈ t → Disjoint (G.neighborFinset w) t$$

Lean4

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

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