isBipartiteWith_neighborFinset_subset'

English

If G.IsBipartiteWith s t and w ∈ t, then neighborFinset w ⊆ s.

Русский

Если G.IsBipartiteWith 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 finset of `w` is a subset of `s`. -/
theorem isBipartiteWith_neighborFinset_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.neighborFinset w ⊆ s :=
  by
  rw [isBipartiteWith_neighborFinset' h hw]
  exact filter_subset (G.Adj · w) s

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