nil_ne_cons — Mathlib

English

If p is a path from a to b and e is an arrow from b to a, then the nil path from a to a is not equal to p extended by e.

Русский

Путь нуль длины из a в a не равен пути p, взятому с последним ребром e: b→a (то есть продолжению p через e).

LaTeX

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

Lean4

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

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