exact

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

← MathLib Explorer

English

If connectedComponentMk v equals connectedComponentMk w, then v is reachable to w.

Русский

Если connectedComponentMk v = connectedComponentMk w, то vReachable w.

LaTeX

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

Lean4

protected theorem exact {v w : V} : G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w :=
  @Quotient.exact _ G.reachableSetoid _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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