mem_of_mem_adj — Mathlib

English

If bipartition with s,t holds and v ∈ s and v adjacent to w, then w ∈ t.

Русский

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

LaTeX

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

Lean4

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

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