isBipartiteWith_neighborSet_disjoint'

English

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

Русский

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

LaTeX

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

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is disjoint to `t`. -/
theorem isBipartiteWith_neighborSet_disjoint' (h : G.IsBipartiteWith s t) (hw : w ∈ t) : Disjoint (G.neighborSet w) t :=
  Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset' h hw) h.disjoint

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