decidableEqBddPathsZero

Mathlib.Combinatorics.Quiver.Path

URI: https://scilib.ai/kg/mathlib#Quiver.Path.decidableEqBddPathsZero

← MathLib Explorer

English

Equality on bounded paths of length zero is decidable.

Русский

Равенство ограниченных путей нулевой длины решаемо.

LaTeX

$$$\\mathrm{DecidableEq}(\\mathrm{BoundedPaths}(v,w,0)).$$$

Lean4

/-- Bounded paths of length zero between two vertices have decidable equality. -/
def decidableEqBddPathsZero (v w : V) : DecidableEq (BoundedPaths v w 0) := fun _ _ => isTrue <| Subsingleton.elim _ _

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

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

Разделы

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

Аффилиация

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