length_toPath

Mathlib.Combinatorics.Quiver.Path

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

English

For any edge e: a → b, the length of its one-step path e.toPath is 1.

Русский

Для любого ребра e: a → b длина пути e.toPath равна 1.

LaTeX

$$$\\forall a,b:\\; e: a\\to b:\\; \\mathrm{length}(e^{\\to\\mathrm{Path}}) = 1.$$$

Lean4

@[simp]
theorem length_toPath {a b : V} (e : a ⟶ b) : e.toPath.length = 1 :=
  rfl

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

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

Разделы

Аффилиация

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