instFiniteConnectedComponent

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting

URI: https://scilib.ai/kg/mathlib#SimpleGraph.instFiniteConnectedComponent

English

If the vertex set is finite, then the collection of connected components is finite.

Русский

Если множество вершин конечное, то множество связных компонент конечно.

LaTeX

$$$\lvert G.ConnectedComponent \rvert < \infty$$$

Lean4

instance [Finite V] : Finite G.ConnectedComponent :=
  Quot.finite _

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

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

Разделы

Аффилиация

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