comp_assoc — Mathlib

English

Path composition is associative: for any p: Path a b, q: Path b c, r: Path c d, (p ∘ q) ∘ r = p ∘ (q ∘ r).

Русский

Составление путей ассоциативно: для любых путей p: a→b, q: b→c, r: c→d выполняется (p ∘ q) ∘ r = p ∘ (q ∘ r).

LaTeX

$$$\\forall p:\\; \\mathrm{Path}(a,b),\\; q:\\; \\mathrm{Path}(b,c),\\; r:\\; \\mathrm{Path}(c,d):\\; (p\\circ q)\\circ r = p\\circ (q\\circ r).$$$

Lean4

@[simp]
theorem comp_assoc {a b c : V} :
    ∀ {d} (p : Path a b) (q : Path b c) (r : Path c d), (p.comp q).comp r = p.comp (q.comp r)
  | _, _, _, nil => rfl
  | _, p, q, cons r _ => by rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

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