instDecidableEq

Mathlib.Combinatorics.Quiver.Path

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

Lean4

/-- Equality is decidable on paths in a quiver given decidable equality on the vertices and
arrows. -/
instance instDecidableEq [DecidableEq V] [∀ (v w : V), DecidableEq (v ⟶ w)] : (v w : V) → DecidableEq (Path v w) :=
  fun v w p q =>
  let m := max p.length q.length
  let p' : BoundedPaths v w m := ⟨p, Nat.le_max_left ..⟩
  let q' : BoundedPaths v w m := ⟨q, Nat.le_max_right ..⟩
  decidable_of_iff (p' = q') Subtype.ext_iff

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

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

Разделы

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

Аффилиация

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