eq_nil_of_length_zero — Mathlib

English

If a path p has length zero, then after transporting along the equality eq_of_length_zero, p becomes Path.nil.

Русский

Если путь p имеет нулевую длину, после переноса по равенству eq_of_length_zero путь становится Path.nil.

LaTeX

$$$ p.cast (eq\\_of\\_length\\_zero\\ p\\ hzero)\\ rfl = Path.nil $$$

Lean4

theorem eq_nil_of_length_zero {u v : U} (p : Path u v) (hzero : p.length = 0) :
    p.cast (eq_of_length_zero p hzero) rfl = Path.nil :=
  by
  cases p
  · rfl
  · simp only [Nat.succ_ne_zero, length_cons] at hzero

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