isBipartiteWith_neighborFinset' — Mathlib

English

Same as above stated in a variant form.

Русский

Те же утверждения в варианте.

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.degree v ≤ |t|$$

Lean4

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

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