instDecidableRelReachable

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting

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

English

For a finite vertex graph, the Reachable relation is decidable.

Русский

Для графа с конечным числом вершин отношение достижимости разрешимо (решимо).

LaTeX

$$$\text{Decidable}(G.Reachable)$$$

Lean4

instance : DecidableRel G.Reachable := fun u v =>
  decidable_of_iff' _ (reachable_iff_exists_finsetWalkLength_nonempty G u v)

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

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

Разделы

Аффилиация

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