isBipartiteWith_neighborFinset_subset

English

Alternative statement expressing the same relation as above.

Русский

Альтернативное выражение того же соотношения.

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.neighborFinset v = bipartiteAbove G.Adj t v$$

Lean4

/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is a subset of `s`. -/
theorem isBipartiteWith_neighborFinset_subset (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G.neighborFinset v ⊆ t :=
  by
  rw [isBipartiteWith_neighborFinset h hv]
  exact filter_subset (G.Adj v ·) t

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