length_nil

Mathlib.Combinatorics.Quiver.Path

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

English

The length of the nil path from a to a is zero.

Русский

Длина нулевого пути от вершины a к самой себе равна нулю.

LaTeX

$$$\\forall a:\\; {\\text{Path}}(a,a):\\; \\mathrm{length}(\\mathrm{nil}) = 0.$$$

Lean4

@[simp]
theorem length_nil {a : V} : (nil : Path a a).length = 0 :=
  rfl

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

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

Разделы

Аффилиация

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