length_vertices_pos

Mathlib.Combinatorics.Quiver.Path.Vertices

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

English

For any nontrivial path p, its vertices list length is strictly positive.

Русский

Для любого ненулевого пути p длина списка вершин строго положительна.

LaTeX

$$length_vertices_pos$$

Lean4

theorem length_vertices_pos {a b : V} (p : Path a b) : 0 < p.vertices.length := by simp

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

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

Разделы

Аффилиация

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