isBipartiteWith_neighborSet_subset

English

If G is bipartite with s,t and v ∈ s, then the neighbor set of v is a subset of t.

Русский

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

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.neighborSet(v) ⊆ t$$

Lean4

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

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