comp_eq_nil_iff — Mathlib

English

A composition equals the nil path if and only if both components are nil paths; equivalently, p.comp q = nil ⇔ p.length = 0 ∧ q.length = 0.

Русский

Композиция равна нулю тогда и только тогда, когда обе части равны нулю; то есть p.comp q = nil ⇔ p.length = 0 and q.length = 0.

LaTeX

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

Lean4

theorem comp_eq_nil_iff {a b : V} {p : Path a b} {q : Path b a} : p.comp q = Path.nil ↔ p.length = 0 ∧ q.length = 0 :=
  by
  refine ⟨fun h ↦ ⟨nil_of_comp_eq_nil_left h, nil_of_comp_eq_nil_right h⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
  induction p with
  | nil => simpa using (length_eq_zero_iff q).mp hq
  | cons p' _ ihp => simp at hp

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