isBipartiteWith_neighborFinset_disjoint'

English

The neighborFinset w equals bipartiteBelow G.Adj s w for the downward view.

Русский

neighborFinset w совпадает с bipartiteBelow G.Adj s w.

LaTeX

$$G.IsBipartiteWith s t → w ∈ t → G.neighborFinset w = bipartiteBelow G.Adj s w$$

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is disjoint to `t`. -/
theorem isBipartiteWith_neighborFinset_disjoint' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
    Disjoint (G.neighborFinset w) t :=
  by
  rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
  exact isBipartiteWith_neighborSet_disjoint' h hw

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