isBipartiteWith_neighborSet_subset'

English

If G is bipartite with s,t and w ∈ t, then neighborFinset(w) ⊆ s.

Русский

Если G двудольный с s и t и w ∈ t, то neighborFinset(w) ⊆ s.

LaTeX

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

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is a subset of `s`. -/
theorem isBipartiteWith_neighborSet_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.neighborSet w ⊆ s :=
  by
  rw [isBipartiteWith_neighborSet' h hw]
  exact Set.sep_subset s (G.Adj · w)

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