connectedComponentMk_eq_of_adj — Mathlib

English

If two vertices are adjacent in G, then they belong to the same connected component; equivalently, their connected component labels are equal.

Русский

Если две вершины смежны в G, то они принадлежат одной и той же компоненте связности; эквивалентно равенству их меток компонент связности.

LaTeX

$$$G.Adj v w \\\\Rightarrow G.connectedComponentMk v = G.connectedComponentMk w$$$

Lean4

theorem connectedComponentMk_eq_of_adj {v w : V} (a : G.Adj v w) :
    G.connectedComponentMk v = G.connectedComponentMk w :=
  ConnectedComponent.sound a.reachable

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