instSubsingletonBddPaths — Mathlib

English

The set of bounded paths of length zero from v to w is a subsingleton.

Русский

Множество ограниченных путей длины ноль между вершинами v и w является подсинглтоном.

LaTeX

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

Lean4

/-- Bounded paths of length zero between two vertices form a subsingleton. -/
instance instSubsingletonBddPaths (v w : V) : Subsingleton (BoundedPaths v w 0) where
  allEq := fun ⟨p, hp⟩ ⟨q, hq⟩ =>
    match v, w, p, q with
    | _, _, .nil, .nil => rfl
    | _, _, .cons _ _, _ => by simp [Quiver.Path.length] at hp
    | _, _, _, .cons _ _ => by simp [Quiver.Path.length] at hq

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