sound

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.sound

English

If v and w are connected, then the corresponding connected components are equal.

Русский

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

LaTeX

$$$\forall v w\; G.Reachable\ v\ w \Rightarrow G.connectedComponentMk v = G.connectedComponentMk w$$$

Lean4

protected theorem sound {v w : V} : G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w :=
  Quot.sound

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru