isBipartiteWith_bipartiteBelow — Mathlib

English

The neighborFinset of w equals bipartiteBelow G.Adj s w when w ∈ t.

Русский

Для w ∈ t, neighborFinset w = bipartiteBelow G.Adj s w.

LaTeX

$$G.IsBipartiteWith s t → w ∈ t → G.neighborFinset w = bipartiteBelow G.Adj s w$$

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
"below" `w` according to the adjacency relation of `G`. -/
theorem isBipartiteWith_bipartiteBelow (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
    G.neighborFinset w = bipartiteBelow G.Adj s w := by rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]

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