isBipartiteWith_neighborSet_disjoint

English

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

Русский

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

LaTeX

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

Lean4

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

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