instFintypeConnectedComponent

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting

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

English

There is a finite-type instance for the set of connected components under a finite vertex set.

Русский

Существует конечный тип компонент связности для графа с конечным числом вершин.

LaTeX

$$$\text{Fintype}(G.ConnectedComponent)$$$

Lean4

instance : Fintype G.ConnectedComponent :=
  @Quotient.fintype _ _ G.reachableSetoid (inferInstance : DecidableRel G.Reachable)

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

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

Разделы

Аффилиация

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