componentComplMk_eq_of_adj — Mathlib

English

If v and w are outside K and adjacent, their outside components are equal.

Русский

Если v и w вне K и смежны, то их внешние компоненты равны.

LaTeX

$$$$ (G : SimpleGraph V) {v w : V} (vK : v \notin K) (wK : w \notin K) (a : G.Adj v w) :\ G.componentComplMk vK = G.componentComplMk wK. $$$$

Lean4

theorem componentComplMk_eq_of_adj (G : SimpleGraph V) {v w : V} (vK : v ∉ K) (wK : w ∉ K) (a : G.Adj v w) :
    G.componentComplMk vK = G.componentComplMk wK :=
  by
  rw [ConnectedComponent.eq]
  apply Adj.reachable
  exact a

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