nil_of_comp_eq_nil_right — Mathlib

English

If p ∘ q is nil, then the right component q must be nil (length zero).

Русский

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

LaTeX

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

Lean4

/-- If a composition is `nil`, the right component must be `nil` -/
theorem nil_of_comp_eq_nil_right {a b : V} {p : Path a b} {q : Path b a} (h : p.comp q = Path.nil) : q.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_left this

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