cons_ne_nil

Mathlib.Combinatorics.Quiver.Path

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

English

For any path p from a to b and edge e: b→a, the extended path p.cons e is not the nil path.

Русский

Для любого пути p: a→b и ребра e: b→a, путь p.cons e нe равен нулю.

LaTeX

$$$\\forall p:\\, \\mathrm{Path}(a,b),\\; \\forall e:\\, b \\to a:\\; p.\\mathrm{cons}(e) \\neq \\mathrm{Path.nil}.$$$

Lean4

theorem cons_ne_nil (p : Path a b) (e : b ⟶ a) : p.cons e ≠ Path.nil := fun h => by injection h

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

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

Разделы

Аффилиация

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