fintypeSubtypeWalkLength

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting

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

English

The subtype of walks of length n is finite.

Русский

Подмножество ходов длины n является конечным.

LaTeX

$$Fintype { p : G.Walk u v // p.length = n }$$

Lean4

instance fintypeSubtypeWalkLength (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length = n } :=
  fintypeSetWalkLength G u v n

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

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

Разделы

Аффилиация

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