mem_of_mem_adj' — Mathlib

English

If G is bipartite with s,t and w ∈ t and v adjacent to w, then v ∈ s.

Русский

Если G двудольный с s и t и w ∈ t и v смежен с w, то v ∈ s.

LaTeX

$$G.IsBipartiteWith s t → w ∈ t → G.Adj v w → v ∈ s$$

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then if `v` is adjacent to `w` in `G` then `v ∈ s`. -/
theorem mem_of_mem_adj' (h : G.IsBipartiteWith s t) (hw : w ∈ t) (hadj : G.Adj v w) : v ∈ s :=
  by
  apply h.mem_of_adj at hadj
  have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
  simpa [hw, nhw] using hadj

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