isBipartiteWith_bipartiteAbove — Mathlib

English

If G is bipartite with s,t and v ∈ s, then neighborFinset(v) equals bipartiteAbove G.Adj t v.

Русский

Если G двудольный с s и t и v ∈ s, то neighborFinset(v) равно bipartiteAbove G.Adj t v.

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.neighborFinset v = bipartiteAbove G.Adj t v$$

Lean4

/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
"above" `v` according to the adjacency relation of `G`. -/
theorem isBipartiteWith_bipartiteAbove (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
    G.neighborFinset v = bipartiteAbove G.Adj t v := by rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]

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