nil_of_comp_eq_nil_left — Mathlib

English

If the composition p ∘ q is nil (the trivial path), then the left component p must be nil (have length zero).

Русский

Если композиция p ⋅ q равна нулю (путь-нулевой), то слева стоящая часть p имеет нулевую длину.

LaTeX

$$$(p.comp\; q) = \mathrm{Path.nil} \Rightarrow p.length = 0$$$

Lean4

/-- If a composition is `nil`, the left component must be `nil`
    (proved via lengths, avoiding dependent pattern-matching). -/
theorem nil_of_comp_eq_nil_left {a b : V} {p : Path a b} {q : Path b a} (h : p.comp q = Path.nil) : p.length = 0 :=
  by
  have hlen : (p.comp q).length = 0 := by simpa using congrArg Path.length h
  have : p.length + q.length = 0 := by simpa [length_comp] using hlen
  exact Nat.eq_zero_of_add_eq_zero_right this

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