eq — Mathlib · SciLib

English

Let G be a simple graph on vertex set V. For any v, w in V, the connected component label of v equals that of w if and only if there exists a path from v to w in G.

Русский

Пусть G — простой граф на вершинах V. Для любых вершин v, w ∈ V метка компонент связности v совпадает с меткой компонент связности w тогда и только тогда между v и w существует путь в G.

LaTeX

$$$\\\\forall v\\\\, w : V,\\\\ G.connectedComponentMk v = G.connectedComponentMk w \\\\iff G.Reachable v w$$$

Lean4

@[simp]
protected theorem eq {v w : V} : G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w :=
  @Quotient.eq' _ G.reachableSetoid _ _

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