comp_inj' — Mathlib

English

For paths p1, p2 from a to b and q1, q2 from b to c, equality of left lengths implies p1.comp q1 = p2.comp q2 iff p1 = p2 and q1 = q2.

Русский

Для путей p1, p2:a→b и q1, q2:b→c равенство левых длин дает p1.comp q1 = p2.comp q2 тогда и только тогда, когда p1 = p2 и q1 = q2.

LaTeX

$$$\text{If } p_1.length = p_2.length,\; p_1.comp q_1 = p_2.comp q_2 \iff p_1 = p_2 \land q_1 = q_2$$$

Lean4

theorem comp_inj' {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (h : p₁.length = p₂.length) :
    p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂ :=
  ⟨fun h_eq => (comp_inj <| Nat.add_left_cancel (n := p₂.length) <| by simpa [h] using congr_arg length h_eq).1 h_eq, by
    rintro ⟨rfl, rfl⟩; rfl⟩

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